src/HOL/thy_syntax.ML
1998-10-21 berghofe 1998-10-21 Changed syntax of rep_datatype and inductive: Theorems are no longer specified by a string of ML type "thm list" but by a comma-separated list of identifiers, which are looked up in the theory.
1998-10-16 berghofe 1998-10-16 Changed structure of name spaces for datatypes.
1998-07-30 berghofe 1998-07-30 Fixed primrec.
1998-07-30 berghofe 1998-07-30 Fixed primrec.
1998-07-30 wenzelm 1998-07-30 fixed primrec;
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-06-30 berghofe 1998-06-30 Adapted to new inductive definition package.
1998-04-29 wenzelm 1998-04-29 TypedefPackage.add_typedef; RecordPackage.add_record;
1998-01-08 oheimb 1998-01-08 added split_paired_Ex to the implicit simpset
1997-11-13 wenzelm 1997-11-13 fixed record parser;
1997-11-13 wenzelm 1997-11-13 improved record syntax;
1997-11-12 oheimb 1997-11-12 renamed split_T_case_prem to split_T_case_asm
1997-11-07 nipkow 1997-11-07 Each datatype t now proves a theorem split_t_case_prem P(t_case f1 ... fn x) = (~((? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) | ... (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn)) ) )
1997-11-03 wenzelm 1997-11-03 tuned;
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-30 nipkow 1997-10-30 For each datatype `t' there is now a theorem `split_t_case' of the form P(t_case f1 ... fn x) = ((!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1))& ... (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))) The simplifier now reduces !x. (..x.. & x = t & ..x..) --> P x to (..t.. & ..t..) --> P t (and similarly for t=x).
1997-10-24 wenzelm 1997-10-24 record: tuned output;
1997-10-23 wenzelm 1997-10-23 added record section;
1997-10-20 wenzelm 1997-10-20 adapted to qualified names;
1997-09-10 nipkow 1997-09-10 Added Larry's test for preventing a datatype shadowing a theory.
1997-08-06 wenzelm 1997-08-06 use ThySyn.add_syntax;
1997-08-06 berghofe 1997-08-06 Replaced "init_thy_reader" by "set_parser".
1997-06-23 paulson 1997-06-23 New "congs" keyword for recdef theory section
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