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"