| Thu, 19 Jun 2008 11:46:14 +0200 | krauss | generalized induct_scheme method to prove conditional induction schemes. | file | diff | annotate |
| Tue, 15 Apr 2008 16:12:05 +0200 | wenzelm | Thm.forall_elim_var(s); | file | diff | annotate |
| Mon, 14 Apr 2008 16:42:47 +0200 | krauss | proper context for induct_scheme method | file | diff | annotate |
| Sun, 09 Dec 2007 20:59:53 +0100 | krauss | added Id, some cleanup | file | diff | annotate |
| Fri, 07 Dec 2007 09:42:20 +0100 | krauss | experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy) | file | diff | annotate |