| Mon, 12 May 2008 22:11:06 +0200 | krauss | Measure functions can now be declared via special rules, allowing for a | file | diff | annotate |
| Fri, 25 Apr 2008 16:28:06 +0200 | krauss | * New attribute "termination_simp": Simp rules for termination proofs | file | diff | annotate |
| Fri, 25 Apr 2008 15:30:33 +0200 | krauss | Merged theories about wellfoundedness into one: Wellfounded.thy | 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 |
| Thu, 06 Dec 2007 12:58:01 +0100 | krauss | load sum_tree.ML | file | diff | annotate |
| Tue, 25 Sep 2007 12:16:08 +0200 | haftmann | datatype interpretators for size and datatype_realizer | file | diff | annotate |
| Thu, 09 Aug 2007 15:52:42 +0200 | haftmann | re-eliminated Option.thy | file | diff | annotate |