src/HOL/thy_syntax.ML
1997-06-05 paulson 1997-06-05 A slight simplification of optstring The new "simpset" keyword in the "recdef" declaration
1997-05-26 paulson 1997-05-26 Now recdef checks the name of the function being defined. Slight tidying
1997-05-23 nipkow 1997-05-23 Added overloaded function `size' for all datatypes.
1997-05-15 paulson 1997-05-15 TFL theory section
1997-04-10 nipkow 1997-04-10 Turned Addsimps into AddIffs for datatype laws.
1997-04-09 paulson 1997-04-09 Using Blast_tac
1996-07-05 berghofe 1996-07-05 Simplified syntax of primrec definitions.
1996-06-06 paulson 1996-06-06 Quotes now optional around inductive set
1996-04-19 clasohm 1996-04-19 added Konrad's code for the datatype package
1996-03-13 clasohm 1996-03-13 modified primrec so it can be used in MiniML/Type.thy
1996-02-05 clasohm 1996-02-05 expanded tabs; renamed subtype to typedef; incorporated Konrad's changes
1996-01-30 clasohm 1996-01-30 expanded tabs
1996-01-02 paulson 1996-01-02 Improving space efficiency of inductive/datatype definitions. Reduce usage of "open" and change struct open X; D end to let open X in struct D end end whenever possible -- removes X from the final structure. Especially needed for functors Intr_elim and Indrule.
1995-11-02 clasohm 1995-11-02 extended complex_typ
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-09-08 clasohm 1995-09-08 added nested types on right hand side of datatype definitions
1995-03-28 clasohm 1995-03-28 changed syntax of datatype declarations (curried types for constructor parameters)
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application