src/HOL/thy_syntax.ML
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