src/HOL/Tools/lin_arith.ML
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
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2007-10-12 webertj 2007-10-12 typo in comment fixed
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-08-18 webertj 2007-08-18 fixed a bug in demult: -a in (-a * b) is no longer treated as atomic
2007-08-14 wenzelm 2007-08-14 avoid low-level tsig;
2007-08-09 haftmann 2007-08-09 localized of_nat
2007-08-01 wenzelm 2007-08-01 simplified internal Config interface;
2007-07-31 wenzelm 2007-07-31 HOL setup for linear arithmetic -- moved here from arith_data.ML;