src/HOL/Tools/record.ML
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;
2011-05-05 bulwahn 2011-05-05 adding creation of exhaustive generators for records; simplifying dependencies in Main theory
2011-04-17 wenzelm 2011-04-17 added Binding.print convenience, which includes quote already;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 prefer local name spaces; tuned signatures; tuned;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-04-06 wenzelm 2011-04-06 typed_print_translation: discontinued show_sorts argument;
2011-04-06 wenzelm 2011-04-06 moved unparse material to syntax_phases.ML;
2011-04-06 wenzelm 2011-04-06 renamed Standard_Syntax to Syntax_Phases;
2011-04-05 wenzelm 2011-04-05 moved decode/parse operations to standard_syntax.ML; tuned;
2011-03-26 wenzelm 2011-03-26 added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent; recovered printing of Hoare assign statements from 45d090186bbe;
2011-03-11 bulwahn 2011-03-11 adaptions in generators using the common functions
2011-03-11 bulwahn 2011-03-11 adapting record package to renaming of quickcheck's structures
2011-01-16 wenzelm 2011-01-16 proper type variables with sorts;
2011-01-15 wenzelm 2011-01-15 recovered printing of record updates over compound terms, e.g. "(|x = a|)(|x := b|)", which was apparently broken in 45a2ffc5911e; tuned;
2011-01-15 wenzelm 2011-01-15 export Record.get_hierarchy -- external tools typically need this information;
2011-01-15 wenzelm 2011-01-15 tuned;