| 2010-09-29 | Christian Urban | simplified exhaust proofs | file | diff | annotate |
| 2010-09-29 | Christian Urban | worked example Foo1 with induct_schema | file | diff | annotate |
| 2010-09-28 | Christian Urban | added Foo1 to explore a contrived example | file | diff | annotate |