2015-11-17 paulson 2015-11-17 Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-06-01 haftmann 2015-06-01 separate class for division operator, with particular syntax added in more specific classes
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-11-28 huffman 2011-11-28 use HOL_basic_ss instead of HOL_ss for internal simproc proofs (cf. b36eedcd1633)
2011-11-11 huffman 2011-11-11 use simproc_setup for the remaining nat_numeral simprocs
2011-11-11 huffman 2011-11-11 use simproc_setup for more nat_numeral simprocs; add simproc tests
2011-11-09 huffman 2011-11-09 use simproc_setup for some nat_numeral simprocs; add simproc tests
2011-10-29 huffman 2011-10-29 remove unused function
2011-10-27 huffman 2011-10-27 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 haftmann 2011-09-17 dropped unused argument – avoids problem with SML/NJ
2011-09-17 haftmann 2011-09-17 tuned
2010-12-02 wenzelm 2010-12-02 renamed trace_simp to simp_trace, and debug_simp to simp_debug;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-06-08 haftmann 2010-06-08 tuned quotes, antiquotations and whitespace
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
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 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-07-23 wenzelm 2009-07-23 more @{theory} antiquotations;
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-06-24 nipkow 2009-06-24 corrected and unified thm names
2009-06-02 wenzelm 2009-06-02 made SML/NJ happy;
2009-05-08 haftmann 2009-05-08 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs