src/HOL/thy_syntax.ML
1997-09-10 ago Added Larry's test for preventing a datatype shadowing a theory.
1997-08-06 ago use ThySyn.add_syntax;
1997-08-06 ago Replaced "init_thy_reader" by "set_parser".
1997-06-23 ago New "congs" keyword for recdef theory section
1997-06-05 ago A slight simplification of optstring
1997-05-26 ago Now recdef checks the name of the function being defined.
1997-05-23 ago Added overloaded function `size' for all datatypes.
1997-05-15 ago TFL theory section
1997-04-10 ago Turned Addsimps into AddIffs for datatype laws.
1997-04-09 ago Using Blast_tac
1996-07-05 ago Simplified syntax of primrec definitions.
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