src/HOL/Induct/LList.thy
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
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-10-12 paulson 2005-10-12 tidying
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-05-09 paulson 2005-05-09 from simplesubst to new subst
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-12-15 paulson 2004-12-15 removal of archaic Abs/Rep proofs
2002-09-26 paulson 2002-09-26 Converted Fun to Isar style. Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy. Renamed constant "Fun.op o" to "Fun.comp"
2002-08-27 wenzelm 2002-08-27 *** empty log message ***
2002-05-07 wenzelm 2002-05-07 tuned presentation;
2002-04-02 paulson 2002-04-02 conversion of some HOL/Induct proof scripts to Isar
2001-01-09 nipkow 2001-01-09 *** empty log message ***
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
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-05-07 paulson 1997-05-07 New directory to contain examples of (co)inductive definitions