src/HOL/ex/Records.thy
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-04-30 Gerwin Klein 2012-04-30 provide [[record_codegen]] option for skipping codegen setup for records
2012-01-15 wenzelm 2012-01-15 tuned example;
2011-04-23 wenzelm 2011-04-23 modernized specifications;
2010-07-27 haftmann 2010-07-27 delete structure Basic_Record; avoid `record` in names in structure Record
2010-07-14 haftmann 2010-07-14 avoid export_code ... file -
2010-01-27 haftmann 2010-01-27 a more complex record expression -- cf. src/HOL/Tools/quickcheck_generators.ML
2009-11-11 haftmann 2009-11-11 explicit invocation of code generation
2009-11-10 haftmann 2009-11-10 tuned header
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-05-24 haftmann 2009-05-24 dropped Id
2008-05-17 wenzelm 2008-05-17 avoid undeclared variables within proofs;
2007-12-19 schirmer 2007-12-19 more examples
2007-04-20 haftmann 2007-04-20 tuned
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-05-27 wenzelm 2006-05-27 tuned;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-06-29 kleing 2004-06-29 license change to BSD
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.
2001-12-21 wenzelm 2001-12-21 qualified point.more;
2001-11-22 wenzelm 2001-11-22 thm "point.defs";
2001-10-25 wenzelm 2001-10-25 updated records;
2001-10-25 wenzelm 2001-10-25 (simp add: point.make_def);
2001-10-06 wenzelm 2001-10-06 * sane numerals (stage 2): plain "num" syntax (removed "#");
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2000-10-30 wenzelm 2000-10-30 tuned;
2000-09-21 wenzelm 2000-09-21 renamed HOL/ex/Points to HOL/ex/Records;