2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2012-07-28 huffman 2012-07-28 move exception handlers outside of let block
2012-07-27 huffman 2012-07-27 move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
2012-07-27 huffman 2012-07-27 replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
2012-07-27 huffman 2012-07-27 give Nat_Arith simprocs proper name bindings by using simproc_setup
2012-07-20 huffman 2012-07-20 make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
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-02-19 haftmann 2010-02-19 moved remaning class operations from Algebras.thy to Groups.thy
2010-02-10 haftmann 2010-02-10 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-02-09 haftmann 2010-02-09 hide fact names clashing with fact names from Group.thy
2010-02-08 haftmann 2010-02-08 hide fact Nat.add_0_right; make add_0_right from Groups priority
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-03-12 haftmann 2009-03-12 vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement