src/HOL/Tools/record_package.ML
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.;
2000-02-24 wenzelm 2000-02-24 rN = "record";
2000-02-22 wenzelm 2000-02-22 proper variant names (admit field "r");
2000-02-15 wenzelm 2000-02-15 fixed sel_upd simproc (less efficient, but more complete);
2000-01-28 wenzelm 2000-01-28 HEADGOAL;
2000-01-28 wenzelm 2000-01-28 replaced FIRSTGOAL by FINDGOAL (backtracking!);
2000-01-05 wenzelm 2000-01-05 replaced HOLogic.termTVar by HOLogic.termT;
1999-08-05 wenzelm 1999-08-05 record_simproc for sel-upd (by Sebastian Nanz); removed record_splitter by default;
1999-06-28 wenzelm 1999-06-28 cond_extern_table;
1999-05-25 wenzelm 1999-05-25 formal comments (still dummy);
1999-05-24 wenzelm 1999-05-24 outer syntax keyword classification; no open OuterParse;
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;