2010-05-05 ago farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-03-28 ago static defaults for configuration options;
2010-03-22 ago removed warning_count (known causes for warnings have been resolved)
2010-03-07 ago modernized structure Object_Logic;
2010-02-28 ago more antiquotations;
2010-02-22 ago merged
2010-02-19 ago moved remaning class operations from Algebras.thy to Groups.thy
2010-02-19 ago renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2010-02-19 ago Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;
2010-02-10 ago moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-02-10 ago moved constants inverse and divide to Ring.thy
2010-02-08 ago renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-02-05 ago more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-28 ago new theory Algebras.thy for generic algebraic structures
2009-11-17 ago Fixed splitting of div and mod on integers (split theorem differed from implementation).
2009-11-16 ago Fixed a typo in a comment.
2009-11-10 ago eliminated some unused/obsolete Args.bang_facts;
2009-11-08 ago tuned;
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-10-29 ago eliminated some old folds;
2009-10-29 ago standardized filter/filter_out;
2009-10-21 ago standardized basic operations on type option;
2009-10-02 ago eliminated dead code;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-09-18 ago tuned const_name antiquotations
2009-08-14 ago Fixed a bug where the simplifier would hang on
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-06-08 ago fast_lin_arith uses proper multiplication instead of unfolding to additions
2009-05-11 ago qualified names for Lin_Arith tactics and simprocs
2009-05-11 ago tuned interface of Lin_Arith
2009-05-09 ago interface changes in linarith.ML
2009-03-26 ago simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-23 ago moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
2009-03-15 ago simplified attribute setup;
2009-03-13 ago simplified method setup;
2009-03-13 ago unified type Proof.method and pervasive METHOD combinators;
2009-03-12 ago vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
2009-03-01 ago use long names for old-style fold combinators;
2009-02-09 ago fix to [arith]
2009-02-09 ago new attribute "arith" for facts supplied to arith.
2009-01-18 ago bug fixes
2009-01-17 ago bug fix
2009-01-01 ago avoid polymorphic equality;
2008-08-28 ago no parameter prefix for class interpretation
2008-05-29 ago added warning_count for issued reconstruction failure messages;
2008-05-18 ago renamed type decompT to decomp;
2008-02-22 ago moved refute_tac to linarith.ML
2008-02-20 ago tuned structures in arith_data.ML
2008-02-11 ago fix spelling
2008-01-15 ago joined theories IntDef, Numeral, IntArith to theory Int
2007-10-12 ago typo in comment fixed
2007-10-09 ago generic Syntax.pretty/string_of operations;
2007-08-18 ago fixed a bug in demult: -a in (-a * b) is no longer treated as atomic
2007-08-14 ago avoid low-level tsig;
2007-08-09 ago localized of_nat
2007-08-01 ago simplified internal Config interface;
2007-07-31 ago HOL setup for linear arithmetic -- moved here from arith_data.ML;