src/HOL/Induct/SList.thy
2007-06-04 haftmann 2007-06-04 authentic syntax for List.append
2007-05-19 haftmann 2007-05-19 constant op @ now named append
2007-02-07 berghofe 2007-02-07 Adapted to changes in Transitive_Closure theory.
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-09-28 wenzelm 2006-09-28 fixed translations: CONST;
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
2004-05-21 wenzelm 2004-05-21 proper use of 'syntax';
2004-04-22 wenzelm 2004-04-22 constdefs: proper order;
2002-09-30 berghofe 2002-09-30 Adapted to new simplifier.
2002-04-04 paulson 2002-04-04 conversion of Induct/{Slist,Sexp} to Isar scripts
2001-11-13 paulson 2001-11-13 new SList theory from Bu Wolff
2001-08-08 paulson 2001-08-08 get it working again using Hilbert_Choice
1999-03-17 wenzelm 1999-03-17 fixed typedef representing set;
1998-11-26 paulson 1998-11-26 tidied up list definitions, using type 'a option instead of unit + 'a, also using real typedefs instead of faking them with extra rules
1998-07-24 berghofe 1998-07-24 Renamed '$' to 'Scons' because of clashes with constants of the same name in theories using datatypes.
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-08-21 paulson 1997-08-21 Renamed set_of_list to set, and relevant theorems too
1997-05-23 nipkow 1997-05-23 Added `arbitrary'
1997-05-07 paulson 1997-05-07 New directory to contain examples of (co)inductive definitions