src/HOL/thy_syntax.ML
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-05-03 schirmer 2004-05-03 reimplementation of HOL records; only one type is created for each record extension, instead of one type for each field. See NEWS.
2004-04-26 wenzelm 2004-04-26 use ThmDatabase.is_ml_identifier;
2004-04-16 berghofe 2004-04-16 Replaced quote by Library.quote, since quote now refers to Symbol.quote
2001-12-14 wenzelm 2001-12-14 record: mixfix;
2001-11-14 wenzelm 2001-11-14 inductive: removed con_defs;
2001-11-04 wenzelm 2001-11-04 tuned comment;
2001-10-17 wenzelm 2001-10-17 improved internal interface of typedef;
2001-10-16 wenzelm 2001-10-16 TypedefPackage.add_typedef_no_result;
2001-09-28 wenzelm 2001-09-28 inductive: no collective atts;
2000-09-05 wenzelm 2000-09-05 RecdefPackage.add_recdef_old;
2000-05-05 wenzelm 2000-05-05 added scan_to_id (used to be in Pure/section_utils.ML);
2000-04-01 wenzelm 2000-04-01 recdef: admit names/atts;
2000-03-30 nipkow 2000-03-30 mod in recdef allows to access the correct simpset via simpset().
1999-05-12 wenzelm 1999-05-12 strip_quotes replaced by unenclose;
1999-05-04 wenzelm 1999-05-04 add_recdef: removed names / attributes;
1999-04-30 wenzelm 1999-04-30 separated recdef / defer_recdef;
1999-04-27 wenzelm 1999-04-27 adapted add_inductive, add_record;
1999-04-23 paulson 1999-04-23 Now for recdefs that omit the WF relation
1999-04-22 wenzelm 1999-04-22 recdef adapted to RecdefPackage.add_recdef;
1999-04-14 wenzelm 1999-04-14 intrs: names and atts;
1999-03-17 wenzelm 1999-03-17 adapted rep_datatype;
1999-03-11 wenzelm 1999-03-11 primrec: empty attributes;
1999-01-12 wenzelm 1999-01-12 get_tthms witness theorems;
1998-12-28 paulson 1998-12-28 replaced obsolete "trim" by "strip_quotes"
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