src/HOL/thy_syntax.ML
2001-11-14 ago inductive: removed con_defs;
2001-11-04 ago tuned comment;
2001-10-17 ago improved internal interface of typedef;
2001-10-16 ago TypedefPackage.add_typedef_no_result;
2001-09-28 ago inductive: no collective atts;
2000-09-05 ago RecdefPackage.add_recdef_old;
2000-05-05 ago added scan_to_id (used to be in Pure/section_utils.ML);
2000-04-01 ago recdef: admit names/atts;
2000-03-30 ago mod in recdef allows to access the correct simpset via simpset().
1999-05-12 ago strip_quotes replaced by unenclose;
1999-05-04 ago add_recdef: removed names / attributes;
1999-04-30 ago separated recdef / defer_recdef;
1999-04-27 ago adapted add_inductive, add_record;
1999-04-23 ago Now for recdefs that omit the WF relation
1999-04-22 ago recdef adapted to RecdefPackage.add_recdef;
1999-04-14 ago intrs: names and atts;
1999-03-17 ago adapted rep_datatype;
1999-03-11 ago primrec: empty attributes;
1999-01-12 ago get_tthms witness theorems;
1998-12-28 ago replaced obsolete "trim" by "strip_quotes"
1998-10-21 ago Changed syntax of rep_datatype and inductive: Theorems
1998-10-16 ago Changed structure of name spaces for datatypes.
1998-07-30 ago Fixed primrec.
1998-07-30 ago Fixed primrec.
1998-07-30 ago fixed primrec;
1998-07-24 ago Adapted to new datatype package.
1998-06-30 ago Adapted to new inductive definition package.
1998-04-29 ago TypedefPackage.add_typedef;
1998-01-08 ago added split_paired_Ex to the implicit simpset
1997-11-13 ago fixed record parser;
1997-11-13 ago improved record syntax;
1997-11-12 ago renamed split_T_case_prem to split_T_case_asm
1997-11-07 ago Each datatype t now proves a theorem split_t_case_prem
1997-11-03 ago tuned;
1997-11-03 ago isatool fixclasimp;
1997-10-30 ago For each datatype `t' there is now a theorem `split_t_case' of the form
1997-10-24 ago record: tuned output;
1997-10-23 ago added record section;
1997-10-20 ago adapted to qualified names;
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