| Wed, 22 Aug 2012 22:55:41 +0200 | wenzelm | prefer ML_file over old uses; | file | diff | annotate |
| Thu, 15 Mar 2012 22:08:53 +0100 | wenzelm | declare command keywords via theory header, including strict checking outside Pure; | file | diff | annotate |
| Thu, 15 Mar 2012 19:02:34 +0100 | wenzelm | declare minor keywords via theory header; | file | diff | annotate |
| Thu, 15 Mar 2012 14:13:49 +0100 | wenzelm | basic support for outer syntax keywords in theory header; | file | diff | annotate |
| Tue, 02 Aug 2011 11:52:57 +0200 | krauss | moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef | file | diff | annotate |
| Tue, 02 Aug 2011 10:36:50 +0200 | krauss | moved recdef package to HOL/Library/Old_Recdef.thy | file | diff | annotate | base |