Sat, 04 Oct 2008 14:58:00 -0400 |
Adam Chlipala |
Try arithmetic contradiction |
Wed, 01 Oct 2008 09:33:44 -0400 |
Adam Chlipala |
Put [try] in front of [subst], to avoid whining about recursive equalities |
Wed, 01 Oct 2008 09:32:36 -0400 |
Adam Chlipala |
Remove [done] markers after enhancement phase finishes |
Tue, 30 Sep 2008 17:47:59 -0400 |
Adam Chlipala |
Co-inductive evaluation example |
Tue, 30 Sep 2008 13:11:39 -0400 |
Adam Chlipala |
Beefed-up crush, with auto-inversion and lemma instantiation |
Sun, 28 Sep 2008 12:44:05 -0400 |
Adam Chlipala |
What could go wrong; some exercises |
Sun, 28 Sep 2008 11:57:15 -0400 |
Adam Chlipala |
Recursive predicates |
Fri, 12 Sep 2008 16:55:37 -0400 |
Adam Chlipala |
Exercises |