src/HOL/Tools/record.ML
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-22 wenzelm 2014-03-22 avoid hard-wired theory names;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-01-01 wenzelm 2014-01-01 clarified simplifier context; eliminated Simplifier.global_context;
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-12-07 haftmann 2013-12-07 default code equations for make, fields, extend and truncate operations on records
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
2013-05-30 wenzelm 2013-05-30 standardized aliases;
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-10 wenzelm 2013-04-10 more standard module name Axclass (according to file name);
2013-03-27 wenzelm 2013-03-27 tuned signature and module arrangement;
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2012-10-12 wenzelm 2012-10-12 discontinued typedef with alternative name;
2012-10-12 wenzelm 2012-10-12 discontinued typedef with implicit set_def;
2012-07-16 wenzelm 2012-07-16 more direct Sorts.has_instance; tuned Sorts.mg_domain;
2012-04-30 Gerwin Klein 2012-04-30 provide [[record_codegen]] option for skipping codegen setup for records
2012-04-26 wenzelm 2012-04-26 tuned comment;
2012-03-30 wenzelm 2012-03-30 tuned;
2012-03-17 wenzelm 2012-03-17 simultaneous read_fields -- e.g. relevant for sort assignment;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-15 wenzelm 2012-03-15 prefer formally checked @{keyword} parser;
2012-03-12 wenzelm 2012-03-12 some grouping of Par_List operations, to adjust granularity;
2012-02-27 wenzelm 2012-02-27 prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
2012-01-15 wenzelm 2012-01-15 comments;
2012-01-15 wenzelm 2012-01-15 eliminated dead code, together with spurious warning about congruence rule for "Fun.comp";
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
2012-01-14 wenzelm 2012-01-14 renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_all_free in favour of plain Logic.all;
2012-01-11 wenzelm 2012-01-11 more qualified names; more antiquotations;
2011-12-30 wenzelm 2011-12-30 tuned;
2011-12-30 wenzelm 2011-12-30 eliminated old-fashioned Global_Theory.add_thms;
2011-12-30 wenzelm 2011-12-30 simplified proof -- avoid res_inst_tac, afford plain asm_full_simp_tac;
2011-12-30 wenzelm 2011-12-30 simplified proof;
2011-12-30 wenzelm 2011-12-30 simplified proof;
2011-12-30 wenzelm 2011-12-30 simplified proof;
2011-12-30 wenzelm 2011-12-30 more parallelism;
2011-12-30 wenzelm 2011-12-30 tuned;
2011-12-29 wenzelm 2011-12-29 tuned -- afford slightly larger simpset in simp_defs_tac;
2011-12-29 wenzelm 2011-12-29 tuned -- standard proofs by default;
2011-12-29 wenzelm 2011-12-29 clarified timeit_msg;
2011-12-29 wenzelm 2011-12-29 tuned;
2011-12-13 wenzelm 2011-12-13 removed dead code;
2011-12-02 wenzelm 2011-12-02 eliminated some legacy operations;
2011-12-02 wenzelm 2011-12-02 more antiquotations;
2011-12-01 bulwahn 2011-12-01 adapting exhaustive generators in record package
2011-11-23 wenzelm 2011-11-23 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-10 wenzelm 2011-11-10 simultaneous check; tight maxidx;
2011-11-09 wenzelm 2011-11-09 sort assignment before simultaneous term_check, not isolated parse_term; prefer Syntax.read_typ over Syntax.parse_typ, to include check phase for sort assignment; simplified Syntax_Phases.decode_sort/decode_typ; discontinued unused Proof_Context.check_tvar;
2011-11-09 wenzelm 2011-11-09 localized Record.decode_type: use standard Proof_Context.get_sort; clarified Record.varifyT: more convential use of maxidx + 1;
2011-09-02 wenzelm 2011-09-02 discontinued slightly odd "Defining record ..." message and corresponding quiet_mode;
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-07-06 wenzelm 2011-07-06 clarified record syntax: fieldext excludes the "more" pseudo-field (unlike 2f885b7e5ba7), so that errors like (| x = a, more = b |) are reported less confusingly;
2011-07-06 wenzelm 2011-07-06 tuned errors; more direct Name.uu_ for dummy abstractions;
2011-07-06 wenzelm 2011-07-06 record package: proper configuration options;
2011-07-06 wenzelm 2011-07-06 just one copy of split_args; tuned error message;
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2011-05-13 wenzelm 2011-05-13 clarified map_simpset versus Simplifier.map_simpset_global;
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;