src/HOL/Tools/record_package.ML
1999-04-30 wenzelm 1999-04-30 theory data: copy;
1999-04-27 wenzelm 1999-04-27 iff_add_global (from simpdata.ML);
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-03-17 wenzelm 1999-03-17 local open OuterParse;
1999-03-11 wenzelm 1999-03-11 outer syntax for 'record'; proof method 'record_split';
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-11-16 wenzelm 1998-11-16 Attribute.thms_of;
1998-10-21 wenzelm 1998-10-21 fixed field_injects;
1998-10-21 wenzelm 1998-10-21 field_injects [iffs];
1998-10-20 wenzelm 1998-10-20 field types: datatype; record_split_tac; quiet_mode; renamed fst/snd to val/more; structure BasicRecordPackage;
1998-08-10 wenzelm 1998-08-10 suffix, unsuffix moved to Pure/library.ML;
1998-08-04 wenzelm 1998-08-04 tuned comments;
1998-07-30 wenzelm 1998-07-30 make_defs not marked as internal;
1998-07-28 wenzelm 1998-07-28 removed global_names flag;
1998-07-27 wenzelm 1998-07-27 tuned;
1998-07-24 wenzelm 1998-07-24 added more_update; added type and update syntax;
1998-06-20 wenzelm 1998-06-20 def_sort;
1998-06-18 wenzelm 1998-06-18 fixed comment;
1998-06-09 wenzelm 1998-06-09 adapted to new theory data interface;
1998-06-05 wenzelm 1998-06-05 accomodate tuned version of theory data;
1998-05-27 paulson 1998-05-27 Changed require to requires for MLWorks
1998-05-26 wenzelm 1998-05-26 foldl_map prep_field;
1998-05-05 wenzelm 1998-05-05 misc tuning;
1998-05-04 wenzelm 1998-05-04 'more' selector; thms: selector_convs, update_convs; tuned;
1998-05-04 wenzelm 1998-05-04 concrete syntax for record terms; defs for update; field types (just abbreviations at the moment); some thms; various of minor improvements;
1998-04-29 wenzelm 1998-04-29 package extensible records with structural subtyping in HOL -- still experimental version;