2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 wenzelm 2010-08-27 merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 wenzelm 2010-08-26 Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
2010-08-26 wenzelm 2010-08-26 slightly more abstract data handling in Fast_Lin_Arith;
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-08-19 haftmann 2010-08-19 tuned quotes
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-07-19 haftmann 2010-07-19 modernized abel_cancel simproc setup
2010-07-19 haftmann 2010-07-19 discontinued pretending that abel_cancel is logic-independent; cleaned up junk
2010-06-08 haftmann 2010-06-08 tuned quotes, antiquotations and whitespace
2010-05-05 haftmann 2010-05-05 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 wenzelm 2010-03-28 static defaults for configuration options;
2010-03-22 boehmes 2010-03-22 removed warning_count (known causes for warnings have been resolved)
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-28 wenzelm 2010-02-28 more antiquotations;
2010-02-22 haftmann 2010-02-22 merged
2010-02-19 haftmann 2010-02-19 moved remaning class operations from Algebras.thy to Groups.thy
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-19 wenzelm 2010-02-19 Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;
2010-02-10 haftmann 2010-02-10 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-02-10 haftmann 2010-02-10 moved constants inverse and divide to Ring.thy
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-11-17 webertj 2009-11-17 Fixed splitting of div and mod on integers (split theorem differed from implementation).
2009-11-16 webertj 2009-11-16 Fixed a typo in a comment.
2009-11-10 wenzelm 2009-11-10 eliminated some unused/obsolete Args.bang_facts;
2009-11-08 wenzelm 2009-11-08 tuned;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-10-02 wenzelm 2009-10-02 eliminated dead code; tuned;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-18 haftmann 2009-09-18 tuned const_name antiquotations
2009-08-14 webertj 2009-08-14 Fixed a bug where the simplifier would hang on lemma "f a = M { nat j |j. 0 <= j & j < f b}" pre_decomp/pre_tac no longer split terms that contain (non-locally) bound variables (e.g., "nat j" in the above example).
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-06-08 boehmes 2009-06-08 fast_lin_arith uses proper multiplication instead of unfolding to additions
2009-05-11 haftmann 2009-05-11 qualified names for Lin_Arith tactics and simprocs
2009-05-11 haftmann 2009-05-11 tuned interface of Lin_Arith
2009-05-09 haftmann 2009-05-09 interface changes in linarith.ML
2009-03-26 wenzelm 2009-03-26 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 haftmann 2009-03-23 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 wenzelm 2009-03-15 simplified attribute setup;
2009-03-13 wenzelm 2009-03-13 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-12 haftmann 2009-03-12 vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-02-09 nipkow 2009-02-09 fix to [arith]
2009-02-09 nipkow 2009-02-09 new attribute "arith" for facts supplied to arith.
2009-01-18 nipkow 2009-01-18 bug fixes
2009-01-17 nipkow 2009-01-17 bug fix
2009-01-01 wenzelm 2009-01-01 avoid polymorphic equality;
2008-08-28 haftmann 2008-08-28 no parameter prefix for class interpretation
2008-05-29 wenzelm 2008-05-29 added warning_count for issued reconstruction failure messages;
2008-05-18 wenzelm 2008-05-18 renamed type decompT to decomp;
2008-02-22 haftmann 2008-02-22 moved refute_tac to linarith.ML
2008-02-20 haftmann 2008-02-20 tuned structures in arith_data.ML
2008-02-11 huffman 2008-02-11 fix spelling