src/HOL/Tools/record.ML
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;
2011-01-15 wenzelm 2011-01-15 removed unreferenced identifiers;
2011-01-10 wenzelm 2011-01-10 standardized split_last/last_elem towards List.last; eliminated obsolete Library.last_elem;
2010-12-01 wenzelm 2010-12-01 just one HOLogic.mk_comp;
2010-12-01 wenzelm 2010-12-01 more direct use of binder_types/body_type;
2010-12-01 wenzelm 2010-12-01 just one Term.dest_funT;
2010-11-26 wenzelm 2010-11-26 make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-11-03 wenzelm 2010-11-03 try_param_tac: plain user error appears more appropriate;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-26 wenzelm 2010-08-26 misc tuning and simplification, notably theory data;
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-08-18 haftmann 2010-08-18 re-added instantiation of type class random for records
2010-08-17 haftmann 2010-08-17 tuned code
2010-08-17 haftmann 2010-08-17 use extension constant as formal constructor of logical record type
2010-08-17 haftmann 2010-08-17 authentic syntax allows simplification of type names
2010-08-17 haftmann 2010-08-17 dropped make_/dest_ naming convention
2010-08-17 haftmann 2010-08-17 formally integrated typecopy layer into record package
2010-08-13 haftmann 2010-08-13 avoid variable name acc (cf. cs. 3142c1e21a0e)
2010-08-09 wenzelm 2010-08-09 tuned comments;
2010-07-27 haftmann 2010-07-27 delete structure Basic_Record; avoid `record` in names in structure Record
2010-07-12 wenzelm 2010-07-12 moved misc legacy stuff from OldGoals to Misc_Legacy; OldGoals: removed unused strip_context, metahyps_thms, read_term, read_prop, gethyps;
2010-06-19 haftmann 2010-06-19 more binding; avoid arcane Rep and Abs prefixes