src/HOL/Tools/record_package.ML
2004-03-03 schirmer 2004-03-03 added record_ex_sel_eq_simproc
2004-01-20 schirmer 2004-01-20 cleaning up
2003-11-06 schirmer 2003-11-06 Records: - Record types are now by default printed with their type abbreviation instead of the list of all field types. This can be configured via the reference "print_record_type_abbr". - Simproc "record_upd_simproc" for simplification of multiple updates added (not enabled by default). - Tactic "record_split_simp_tac" to split and simplify records added. - Bug-fix and optimisation of "record_simproc". - "record_simproc" and "record_upd_simproc" are now sensitive to quick_and_dirty flag.
2003-06-29 berghofe 2003-06-29 - record_split_tac now also works for object-level universal quantifier - bound variables in split rule now have nicer names - added new simproc record_eq_simproc which prevents simplifier from choosing the "wrong" equality rule
2003-04-08 berghofe 2003-04-08 try_param_tac now precomputes substitution for rule, in order to avoid problems with higher order unification.
2002-08-06 wenzelm 2002-08-06 sane interface for simprocs;
2002-07-24 wenzelm 2002-07-24 tuned;
2002-07-24 wenzelm 2002-07-24 adapted fact names;
2002-07-10 wenzelm 2002-07-10 NameSpace.accesses';
2002-02-12 wenzelm 2002-02-12 got rid of explicit marginal comments (now stripped earlier from input);
2001-12-21 wenzelm 2001-12-21 hide base name of "make", "fields", "extend", "truncate", "more", "more_update";
2001-12-14 wenzelm 2001-12-14 mixfix syntax for selectors;
2001-12-10 berghofe 2001-12-10 Added support for code generation.
2001-12-05 wenzelm 2001-12-05 ContextRules.intro_bang_global;
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-27 wenzelm 2001-11-27 make SML/NJ happy;
2001-11-22 wenzelm 2001-11-22 recovered original "make"; added "fields" operation; renamed "derived_defs" to "defs";
2001-11-20 wenzelm 2001-11-20 tuned;
2001-11-20 wenzelm 2001-11-20 derive cases/induct rules for ``more'' parts;
2001-11-09 wenzelm 2001-11-09 fixed print_records;
2001-11-08 wenzelm 2001-11-08 theory data: finish method;
2001-10-27 wenzelm 2001-10-27 use Tactic.prove; improved proof of equality rule;
2001-10-27 wenzelm 2001-10-27 exclude field_simps from user-level "simps";
2001-10-25 wenzelm 2001-10-25 removed "more" sort; refer to properly named theorems internally;
2001-10-25 wenzelm 2001-10-25 derived operations are now: make, extend, truncate (cf. derived_defs);
2001-10-25 wenzelm 2001-10-25 provodes induct/cases for use with corresponding Isar methods; "record" operation (acts as type cast); internal field_inducts, field_cases; make_defs no longer declared as simps; fixed printing of fixed records;
2001-10-24 wenzelm 2001-10-24 moved lambda to Pure/term.ML;
2001-10-18 wenzelm 2001-10-18 tuned;
2001-10-18 wenzelm 2001-10-18 use abstract product type instead of datatype;
2001-10-13 wenzelm 2001-10-13 Drule.tag_internal;
2001-08-08 wenzelm 2001-08-08 field_name_ast_tr superceded by constify_ast_tr in Pure;
2001-08-07 wenzelm 2001-08-07 fix problem with user translations by making field names appear as consts;
2000-09-17 wenzelm 2000-09-17 Display.pretty_thm_sg;
2000-09-07 wenzelm 2000-09-07 tuned;
2000-08-28 wenzelm 2000-08-28 Method.SIMPLE_METHOD';
2000-08-17 wenzelm 2000-08-17 sel_upd proc: include 'more' pseudo-field; added equality rule;
2000-07-13 wenzelm 2000-07-13 adapted PureThy.add_defs_i;
2000-07-01 wenzelm 2000-07-01 GPLed;
2000-06-06 wenzelm 2000-06-06 pair split: proper names of params;
2000-04-17 wenzelm 2000-04-17 Pretty.chunks;
2000-03-25 wenzelm 2000-03-25 export updateN;
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;