2012-03-25 ago merged fork with new numeral representation (see NEWS)
2011-11-28 ago use HOL_basic_ss instead of HOL_ss for internal simproc proofs (cf. b36eedcd1633)
2011-11-11 ago use simproc_setup for the remaining nat_numeral simprocs
2011-11-11 ago use simproc_setup for more nat_numeral simprocs; add simproc tests
2011-11-09 ago use simproc_setup for some nat_numeral simprocs; add simproc tests
2011-10-29 ago remove unused function
2011-10-27 ago fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
2011-09-17 ago dropped unused argument – avoids problem with SML/NJ
2011-09-17 ago tuned
2010-12-02 ago renamed trace_simp to simp_trace, and debug_simp to simp_debug;
2010-08-28 ago formerly unnamed infix equality now named HOL.eq
2010-06-08 ago tuned quotes, antiquotations and whitespace
2010-02-27 ago modernized structure Term_Ord;
2010-02-19 ago moved remaning class operations from Algebras.thy to Groups.thy
2010-02-10 ago moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-02-09 ago hide fact names clashing with fact names from Group.thy
2010-02-08 ago renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-01-28 ago new theory Algebras.thy for generic algebraic structures
2009-07-23 ago more @{theory} antiquotations;
2009-07-15 ago more antiquotations;
2009-06-24 ago corrected and unified thm names
2009-06-02 ago made SML/NJ happy;
2009-05-08 ago modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs