src/HOL/ex/Arith_Examples.thy
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