src/HOL/Tools/record.ML
2010-03-27 wenzelm 2010-03-27 Typedef.info: separate global and local part, only the latter is transformed by morphisms;
2010-03-27 wenzelm 2010-03-27 moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;
2010-03-13 wenzelm 2010-03-13 global typedef;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-06 wenzelm 2010-03-06 record_type_tr': more robust strip_fields (printed types are not necessarily well-formed, e.g. in Syntax.pretty_arity);
2010-03-06 wenzelm 2010-03-06 record_type_abbr_tr': removed obsolete workaround for decode_type, which now retains syntactic categories of variables vs. constructors (authentic syntax);
2010-03-03 wenzelm 2010-03-03 adapted to authentic syntax -- actual types are verbatim;
2010-02-28 wenzelm 2010-02-28 more antiquotations;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2010-02-25 wenzelm 2010-02-25 explicit @{type_syntax} markup;
2010-02-21 wenzelm 2010-02-21 slightly more abstract syntax mark/unmark operations;
2010-02-19 wenzelm 2010-02-19 tuned;
2010-02-19 wenzelm 2010-02-19 authentic term syntax; more precise treatment of naming vs. binding; misc tuning;
2010-02-19 wenzelm 2010-02-19 renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2010-02-16 wenzelm 2010-02-16 simplified/clarified record print translations;
2010-02-16 wenzelm 2010-02-16 eliminated camel case;
2010-02-16 wenzelm 2010-02-16 tuned;
2010-02-16 wenzelm 2010-02-16 simplified/clarified record translations;
2010-02-16 wenzelm 2010-02-16 moved generic update_name to Pure syntax -- not specific to HOL/record;
2010-02-16 wenzelm 2010-02-16 tuned;
2010-02-16 wenzelm 2010-02-16 conceal internal record definitions;
2010-02-15 wenzelm 2010-02-15 refined and exported record_info;
2010-02-15 wenzelm 2010-02-15 modernized structures;
2010-02-15 wenzelm 2010-02-15 modernized signature -- proper binding; misc tuning;
2010-02-15 wenzelm 2010-02-15 tuned errors; tuned;
2010-02-15 wenzelm 2010-02-15 formal markup of constants; misc tuning;
2010-02-15 wenzelm 2010-02-15 eliminated old fold;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-12-21 haftmann 2009-12-21 prefer prefix "iso" over potentially misleading "is"; tuned
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-16 wenzelm 2009-11-16 guard future proofs by Goal.future_enabled;
2009-11-14 schirmer 2009-11-14 clarified quick-and-dirty usage in record package; removed non-optimized versions of proofs; introduced future proofs
2009-11-11 haftmann 2009-11-11 adding code equations for constructors
2009-11-10 haftmann 2009-11-10 substantial simplification restores code generation
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-11-02 wenzelm 2009-11-02 modernized structure Primitive_Defs;
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-22 haftmann 2009-10-22 map_range (and map_index) combinator
2009-10-21 blanchet 2009-10-21 merged
2009-10-21 blanchet 2009-10-21 removed "nitpick_const_simp" attribute from Record's "simps"; Nitpick has its own notion of a record and doesn't need those.
2009-10-21 haftmann 2009-10-21 curried inter as canonical list operation (beware of argument order)
2009-10-21 haftmann 2009-10-21 merged
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-20 wenzelm 2009-10-20 uniform use of Integer.min/max;
2009-10-17 wenzelm 2009-10-17 tuned;
2009-10-17 wenzelm 2009-10-17 removed separate record_quick_and_dirty_sensitive;
2009-10-17 wenzelm 2009-10-17 simplified tactics; use proper SUBGOAL/CSUBGOAL;
2009-10-17 wenzelm 2009-10-17 eliminated old List.foldr and OldTerm operations; misc tuning;
2009-10-17 wenzelm 2009-10-17 removed unused names;
2009-10-17 wenzelm 2009-10-17 misc tuning and simplification;
2009-10-17 wenzelm 2009-10-17 operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
2009-10-17 wenzelm 2009-10-17 explicitly qualify Drule.standard;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-10-01 wenzelm 2009-10-01 avoid mixed l/r infixes, which do not work in some versions of SML;
2009-10-01 wenzelm 2009-10-01 tuned;
2009-10-01 wenzelm 2009-10-01 eliminated dead code, redundant bindings and parameters; use === term operator, which is defined here; handle Type.TYPE_MATCH, not arbitrary exceptions; misc tuning and simplification;
2009-09-30 wenzelm 2009-09-30 made SML/NJ happy;