src/HOL/Datatype.thy
2006-10-16 haftmann 2006-10-16 moved HOL code generator setup to Code_Generator
2006-10-02 haftmann 2006-10-02 clarified setup name
2006-10-01 wenzelm 2006-10-01 merged with theory Datatype_Universe;
2006-09-30 wenzelm 2006-09-30 removed obsolete sum_case_Inl/Inr; moved 'hide' to Datatype_Universe; tuned proofs;
2006-09-19 haftmann 2006-09-19 added operational equality
2006-09-13 krauss 2006-09-13 Major update to function package, including new syntax and the (only theoretical) ability to handle local contexts.
2006-09-01 haftmann 2006-09-01 final syntax for some Isar code generator keywords
2006-07-12 haftmann 2006-07-12 adaptions in codegen
2006-06-14 haftmann 2006-06-14 slight adaption for code generator
2006-06-07 haftmann 2006-06-07 slight code generator cleanup
2006-06-06 haftmann 2006-06-06 improved code lemmas
2006-06-05 krauss 2006-06-05 HOL/Tools/function_package: Added support for mutual recursive definitions.
2006-05-05 krauss 2006-05-05 First usable version of the new function definition package (HOL/function_packake/...). Moved Accessible_Part.thy from Library to Main.
2006-04-06 haftmann 2006-04-06 adapted for definitional code generation
2006-03-07 haftmann 2006-03-07 substantial improvement in codegen iml
2006-03-03 nipkow 2006-03-03 changed and retracted change of location of code lemmas.
2006-02-27 haftmann 2006-02-27 class package and codegen refinements
2006-02-25 haftmann 2006-02-25 improved codegen bootstrap
2006-02-20 haftmann 2006-02-20 slight code generator serialization improvements
2006-01-23 haftmann 2006-01-23 removed problematic keyword 'atom'
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2006-01-04 nipkow 2006-01-04 Reversed Larry's option/iff change.
2005-12-21 paulson 2005-12-21 removed or modified some instances of [iff]
2005-11-22 wenzelm 2005-11-22 Datatype_Universe: hide base names only;
2005-10-17 wenzelm 2005-10-17 change_claset/simpset;
2005-09-17 wenzelm 2005-09-17 lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2003-12-04 nipkow 2003-12-04 hide Push
2003-09-26 paulson 2003-09-26 misc tidying
2003-09-14 nipkow 2003-09-14 Added new theorems
2002-10-10 berghofe 2002-10-10 Added functions Suml and Sumr which are useful for constructing datatypes involving function types.
2002-02-21 wenzelm 2002-02-21 theory Option has been assimilated by Datatype;
2001-11-03 wenzelm 2001-11-03 tuned;
2001-10-27 wenzelm 2001-10-27 made new-style theory; tuned;
2000-10-12 nipkow 2000-10-12 *** empty log message ***
1998-10-23 berghofe 1998-10-23 unit and bool are now represented as datatypes.
1998-10-21 berghofe 1998-10-21 Changed syntax of rep_datatype.
1998-07-24 berghofe 1998-07-24 New theory Datatype. Needed as an ancestor when defining datatypes.