| Tue, 02 Aug 2011 10:36:50 +0200 | krauss | moved recdef package to HOL/Library/Old_Recdef.thy | file | diff | annotate |
| Tue, 03 Aug 2010 18:52:42 +0200 | wenzelm | modernized specifications; | file | diff | annotate |
| Wed, 07 May 2008 10:57:19 +0200 | berghofe | Adapted to encoding of sets as predicates | file | diff | annotate |
| Wed, 03 Oct 2007 19:36:05 +0200 | wenzelm | modernized specifications; | file | diff | annotate |
| Sat, 18 Aug 2007 17:42:39 +0200 | wenzelm | removed obsolete ML bindings; | file | diff | annotate |
| Thu, 17 May 2007 22:37:34 +0200 | krauss | added pointer to new Unification theory | file | diff | annotate |
| Mon, 05 Jun 2006 14:22:58 +0200 | krauss | Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure". | file | diff | annotate |