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-02-28 wenzelm 2010-02-28 more antiquotations; eliminated legacy ML bindings;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2010-02-13 wenzelm 2010-02-13 modernized structures;
2010-02-11 wenzelm 2010-02-11 numeral syntax: clarify parse trees vs. actual terms; modernized translations; formal markup of @{syntax_const} and @{const_syntax};
2010-02-07 wenzelm 2010-02-07 prefer explicit @{lemma} over adhoc forward reasoning;
2009-10-17 wenzelm 2009-10-17 explicitly qualify Drule.standard;
2009-07-23 wenzelm 2009-07-23 more @{theory} antiquotations;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-03-20 wenzelm 2009-03-20 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-06-16 wenzelm 2008-06-16 converted ML proofs;
2008-06-11 wenzelm 2008-06-11 OldGoals.inst;
2008-03-01 wenzelm 2008-03-01 tuned ML code, more antiquotations;
2008-02-11 wenzelm 2008-02-11 removed unnecessary theory qualifiers;
2008-02-11 krauss 2008-02-11 Made theory names in ZF disjoint from HOL theory names to allow loading both developments in a single session (but not merge them).
2007-10-07 wenzelm 2007-10-07 modernized specifications; removed legacy ML bindings;
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated, integer);
2007-05-31 wenzelm 2007-05-31 moved Integ files to canonical place;