src/HOL/thy_syntax.ML
1996-06-06 ago Quotes now optional around inductive set
1996-04-19 ago added Konrad's code for the datatype package
1996-03-13 ago modified primrec so it can be used in MiniML/Type.thy
1996-02-05 ago expanded tabs; renamed subtype to typedef;
1996-01-30 ago expanded tabs
1996-01-02 ago Improving space efficiency of inductive/datatype definitions.
1995-11-02 ago extended complex_typ
1995-10-04 ago added local simpsets; removed IOA from 'make test'
1995-09-08 ago added nested types on right hand side of datatype definitions
1995-03-28 ago changed syntax of datatype declarations (curried types for constructor
1995-03-03 ago new version of HOL with curried function application