src/HOL/Record.thy
2014-09-11 blanchet 2014-09-11 updated news
2014-09-03 blanchet 2014-09-03 use 'datatype_new' in 'Main'
2014-04-25 wenzelm 2014-04-25 modernized theory setup;
2014-03-11 blanchet 2014-03-11 moved 'Quickcheck_Narrowing' further down the theory graph
2014-03-11 blanchet 2014-03-11 make it possible to load Quickcheck exhaustive & narrowing in parallel
2014-01-20 blanchet 2014-01-20 tuning
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
2013-02-14 haftmann 2013-02-14 abandoned theory Plain
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-05-08 bulwahn 2012-05-08 specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2011-09-13 huffman 2011-09-13 tuned proofs
2011-06-09 bulwahn 2011-06-09 adding theory Quickcheck_Narrowing to HOL-Main image
2011-05-05 bulwahn 2011-05-05 adding creation of exhaustive generators for records; simplifying dependencies in Main theory
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");