src/HOL/Record.thy
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.