| Fri, 13 Mar 2009 23:50:05 +0100 | wenzelm | simplified method setup; | file | diff | annotate |
| Fri, 13 Mar 2009 19:58:26 +0100 | wenzelm | unified type Proof.method and pervasive METHOD combinators; | file | diff | annotate |
| Fri, 13 Mar 2009 15:50:06 +0100 | wenzelm | provide regular ML interfaces for Isar source language elements; | file | diff | annotate |
| 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 |