src/HOL/Tools/record_package.ML
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;
2005-06-13 schirmer 2005-06-13 more timing information
2005-06-11 wenzelm 2005-06-11 refer to name spaces values instead of names;
2005-06-09 wenzelm 2005-06-09 Sign.read_typ_abbrev;
2005-06-05 schirmer 2005-06-05 bugfix in record_type_abbr_tr'
2005-05-31 wenzelm 2005-05-31 renamed cond_extern to extern; NameSpace.qualified;
2005-05-13 schirmer 2005-05-13 Bugfix in syntax translation for record type.
2005-05-02 schirmer 2005-05-02 Removed nodup_vars avoiding hack
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-11-05 schirmer 2004-11-05 * extended interface of record_split_simp_tac and record_split_simproc * improved record_type_abbr_tr'
2004-10-26 berghofe 2004-10-26 Removed code generator stuff. Code generation is now handled by code generator in typedef_package.
2004-10-15 schirmer 2004-10-15 record_split_simp_tac now can get simp rules as parameter
2004-09-29 schirmer 2004-09-29 tuned performance of record definition
2004-09-22 schirmer 2004-09-22 bug-fix
2004-07-18 schirmer 2004-07-18 tuned
2004-07-16 schirmer 2004-07-16 added: get_extT_fields and get_recT_fields
2004-07-06 schirmer 2004-07-06 * record_upd_simproc also simplifies trivial updates: r(|x := x r|) = r * tuned quick and dirty mode
2004-06-30 schirmer 2004-06-30 Added reference record_definition_quick_and_dirty_sensitive, to skip proofs triggered by a record definition, if quick_and_dirty is enabled.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-17 schirmer 2004-06-17 tuned
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2004-05-06 schirmer 2004-05-06 tuned HOL/record package; enabled record_upd_simproc by default.
2004-05-04 schirmer 2004-05-04 solved sml-nj compatibility problem
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.
2004-04-22 wenzelm 2004-04-22 tuned;
2004-04-16 wenzelm 2004-04-16 tuned;
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;