src/HOL/ex/Arith_Examples.thy
2011-09-02 wenzelm 2011-09-02 proper config option linarith_trace;
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 Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
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-05-08 haftmann 2009-05-08 explicit method linarith
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
2007-08-18 webertj 2007-08-18 fixed a bug in demult: -a in (-a * b) is no longer treated as atomic
2007-07-31 wenzelm 2007-07-31 tuned LinArith setup;
2007-07-31 wenzelm 2007-07-31 arith method setup: proper context;
2007-06-03 wenzelm 2007-06-03 use antiquotations instead of raw TeX code; tuned document;
2007-06-03 nipkow 2007-06-03 fixed tex error
2007-06-02 webertj 2007-06-02 extended
2007-06-02 webertj 2007-06-02 extended
2007-06-02 webertj 2007-06-02 tracing disabled
2007-06-01 webertj 2007-06-01 some tests for arith added