2010-12-17 wenzelm 2010-12-17 replaced command 'nonterminals' by slightly modernized version 'nonterminal';
2010-08-18 haftmann 2010-08-18 removed separate quickcheck_record module
2010-08-17 haftmann 2010-08-17 dropped make_/dest_ naming convention
2010-08-17 haftmann 2010-08-17 eliminated typecopy interpretation
2010-08-12 haftmann 2010-08-12 moved Record.thy from session Plain to Main; avoid variable name acc
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-02-16 wenzelm 2010-02-16 simplified/clarified record translations;
2010-02-16 wenzelm 2010-02-16 moved generic update_name to Pure syntax -- not specific to HOL/record;
2010-02-16 wenzelm 2010-02-16 tuned;
2010-02-15 wenzelm 2010-02-15 tuned document;
2009-12-21 haftmann 2009-12-21 prefer prefix "iso" over potentially misleading "is"; tuned
2009-11-10 haftmann 2009-11-10 substantial simplification restores code generation
2009-10-01 wenzelm 2009-10-01 eliminated dead code, redundant bindings and parameters; use === term operator, which is defined here; handle Type.TYPE_MATCH, not arbitrary exceptions; misc tuning and simplification;
2009-09-29 wenzelm 2009-09-29 replaced meta_iffD2 by existing Drule.equal_elim_rule2; replaced SymSymTab by existing Symreltab; more antiquotations; eliminated old-style Library.foldl, Library.foldl_map; tuned;
2009-09-29 wenzelm 2009-09-29 tuned header;
2009-09-28 Thomas Sewell 2009-09-28 Fix unescaped expressions breaking latex output in Record.thy Expressions containing _ and ^ need to be adjusted or antiquoted in text comments for latex compatibility. This is in fact a little annoying, since it makes the comment less readable in both source and HTML form.
2009-09-23 tsewell 2009-09-23 Initial response to feedback from Norbert, Makarius on record patch As Norbert recommended, the IsTuple.thy and istuple_support.ML files have been integrated into Record.thy and record.ML. I haven't merged the structures - record.ML now contains Record and IsTupleSupport. Some of the cosmetic changes Makarius requested have been made, including renaming variables with camel-case and run-together names and removing the tab character from the Author: line. Constants are defined with definition rather than constdefs. The split_ex_prf inner function has been cleaned up.
2009-09-10 Thomas Sewell 2009-09-10 Simplification of various aspects of the IsTuple component of the new record package. Extensive documentation added in IsTuple.thy - it should now be possible to figure out what's going on from the sources supplied.
2009-09-10 Thomas Sewell 2009-09-10 Record patch imported and working.
2009-08-27 tsewell 2009-08-27 Initial attempt at porting record update to repository Isabelle.
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2007-12-19 schirmer 2007-12-19 replaced K_record by lambda term %x. c
2007-04-26 wenzelm 2007-04-26 added header;
2007-04-20 haftmann 2007-04-20 reverted to classical syntax for K_record
2007-04-20 haftmann 2007-04-20 Isar definitions are now added explicitly to code theorem table
2006-11-07 schirmer 2006-11-07 field-update in records is generalised to take a function on the field rather than the new value.
2005-10-21 wenzelm 2005-10-21 avoid home-grown meta_allE;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-05-30 wenzelm 2005-05-30 tuned;
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-05-04 schirmer 2004-05-04 tuned;
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.
2003-06-29 berghofe 2003-06-29 Added split_paired_All rule for splitting variables bound by object-level universal quantifiers.
2002-07-24 wenzelm 2002-07-24 simplified locale predicates;
2002-07-24 wenzelm 2002-07-24 predicate defs via locales;
2001-10-27 wenzelm 2001-10-27 removed "more" class;
2001-10-18 wenzelm 2001-10-18 tuned;
2001-10-18 wenzelm 2001-10-18 proper setup for abstract product types;
2001-10-17 wenzelm 2001-10-17 abstract product types;
2001-08-08 wenzelm 2001-08-08 _constify;
2001-08-07 wenzelm 2001-08-07 fix problem with user translations by making field names appear as consts;
2000-12-11 wenzelm 2000-12-11 added "_update_name" and parse_translation;
2000-10-25 wenzelm 2000-10-25 more "xsymbols" syntax;
2000-10-23 wenzelm 2000-10-23 intro_classes by default;
2000-09-27 wenzelm 2000-09-27 more symbolic syntax (currently "input");
2000-08-29 wenzelm 2000-08-29 \<dots> syntax;
1999-08-25 wenzelm 1999-08-25 proper bootstrap of HOL theory and packages;
1998-10-22 wenzelm 1998-10-22 tuned block indent;
1998-10-20 wenzelm 1998-10-20 Datatype instead of Prod;
1998-07-28 wenzelm 1998-07-28 removed global_names flag;
1998-07-24 wenzelm 1998-07-24 added type and update syntax;
1998-06-12 wenzelm 1998-06-12 changed {: :} syntax to (| |);
1998-04-29 wenzelm 1998-04-29 Extensible records with structural subtyping in HOL. See Tools/record_package.ML for the actual implementation.