| Sat, 27 Dec 2008 17:49:15 +0100 | krauss | removed duplicate sum_case used only by function package; | file | diff | annotate |
| Thu, 26 Jun 2008 11:58:27 +0200 | krauss | fix: need to beta/eta normalize | file | diff | annotate |
| Mon, 23 Jun 2008 23:45:39 +0200 | wenzelm | Logic.all/mk_equals/mk_implies; | file | diff | annotate |
| 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 |