src/HOL/Induct/Sexp.thy
2014-01-16 blanchet 2014-01-16 adapted to move of Wfrec
2011-09-13 noschinl 2011-09-13 tune simpset for Complete_Lattices
2011-08-02 krauss 2011-08-02 moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef
2011-08-02 krauss 2011-08-02 moved recdef package to HOL/Library/Old_Recdef.thy
2011-02-22 wenzelm 2011-02-22 modernized specifications;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-10-01 wenzelm 2006-10-01 removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
2006-09-30 wenzelm 2006-09-30 proper import of Main HOL;
2006-05-27 wenzelm 2006-05-27 tuned;
2005-12-15 wenzelm 2005-12-15 removed obsolete/unused setup_induction;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2002-04-04 paulson 2002-04-04 conversion of Induct/{Slist,Sexp} to Isar scripts
2001-08-08 paulson 2001-08-08 get it working again using Hilbert_Choice
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-05-08 wenzelm 2000-05-08 moved theory Sexp to Induct examples;