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 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;
2009-09-29 wenzelm 2009-09-29 removed dead/duplicate code;
2009-09-29 wenzelm 2009-09-29 modernized Balanced_Tree;
2009-09-29 wenzelm 2009-09-29 replaced meta_iffD2 by existing Drule.equal_elim_rule2; replaced SymSymTab by existing Symreltab; more antiquotations; eliminated old-style Library.foldl, Library.foldl_map; tuned;
2009-09-29 wenzelm 2009-09-29 tuned header;
2009-09-29 wenzelm 2009-09-29 tuned whitespace -- recover basic Isabelle conventions;
2009-09-29 wenzelm 2009-09-29 merged
2009-09-29 Thomas Sewell 2009-09-29 Replace OldTerm.term_vars with Term.add_vars in named_cterm_instantiate.
2009-09-28 Thomas Sewell 2009-09-28 Avoid a possible variable name conflict in instantiating a theorem. Instantiating a theorem variable with new variables created a possible variable name conflict if a record was defined with a field named 'f', 'x' etc. Using variable indices of 1 avoids the problem.
2009-09-23 tsewell 2009-09-23 Initial response to feedback from Norbert, Makarius on record patch As Norbert recommended, the IsTuple.thy and istuple_support.ML files have been integrated into Record.thy and record.ML. I haven't merged the structures - record.ML now contains Record and IsTupleSupport. Some of the cosmetic changes Makarius requested have been made, including renaming variables with camel-case and run-together names and removing the tab character from the Author: line. Constants are defined with definition rather than constdefs. The split_ex_prf inner function has been cleaned up.
2009-09-11 Thomas Sewell 2009-09-11 Implement previous fix (don't duplicate ext_def) correctly.
2009-09-11 Thomas Sewell 2009-09-11 There's no particular reason to duplicate the extension constant's definition under the name "ext_def", and it also prevents you having a field called ext.
2009-09-10 Thomas Sewell 2009-09-10 Simplification of various aspects of the IsTuple component of the new record package. Extensive documentation added in IsTuple.thy - it should now be possible to figure out what's going on from the sources supplied.
2009-09-10 Thomas Sewell 2009-09-10 Record patch imported and working.
2009-08-27 tsewell 2009-08-27 Initial attempt at porting record update to repository Isabelle.
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-08-07 wenzelm 2009-08-07 tuned spacing of sections; reduced line length;
2009-07-30 wenzelm 2009-07-30 qualified Subgoal.FOCUS;
2009-07-26 wenzelm 2009-07-26 replaced old METAHYPS by FOCUS;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-02 wenzelm 2009-07-02 renamed NamedThmsFun to Named_Thms; simplified/unified names of instances of Named_Thms;
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"