7 commits

Author	SHA1	Message	Date
Adam Chlipala	65b817d7ae	Revising for Wednesday's lecture	2022-02-06 13:03:43 -05:00
Adam Chlipala	f428750fdf	Change notation to remain compatible with multiple Coq versions	2022-01-31 21:02:31 -05:00
Adam Chlipala	d3c7a85b49	More cleanup around addition of RuleInduction	2021-03-01 12:15:34 -05:00
Adam Chlipala	890d7610d7	End of RuleInduction book chapter	2021-02-28 21:05:05 -05:00
Adam Chlipala	a55a98b426	RuleInduction: some propositional logic, with slightly naughty use of excluded middle	2021-02-28 17:19:06 -05:00
Adam Chlipala	7a906b1a63	Nicer proof of Permutation_app	2021-02-28 11:02:46 -05:00
Adam Chlipala	cf7d27417d	Start code for new RuleInduction chapter, up through permutation	2021-02-28 10:59:13 -05:00