2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 clarified signature;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2013-11-04 haftmann 2013-11-04 streamlined setup of linear arithmetic
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-03-30 huffman 2012-03-30 add constant pred_numeral k = numeral k - (1::nat); replace several simp rules from Nat_Numeral.thy with new ones that use pred_numeral
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-06-29 wenzelm 2011-06-29 modernized some simproc setup;
2011-05-13 wenzelm 2011-05-13 clarified map_simpset versus Simplifier.map_simpset_global;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-26 wenzelm 2010-08-26 Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
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-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
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-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-10-28 haftmann 2009-10-28 moved theory Divides after theory Nat_Numeral; tuned some proof texts
2009-09-18 haftmann 2009-09-18 tuned const_name antiquotations
2009-06-08 boehmes 2009-06-08 fast_lin_arith uses proper multiplication instead of unfolding to additions
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 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
2009-04-29 huffman 2009-04-29 reimplement reorientation simproc using theory data
2009-03-30 huffman 2009-03-30 simplify theorem references
2009-03-26 huffman 2009-03-26 parameterize assoc_fold with is_numeral predicate
2009-03-23 haftmann 2009-03-23 structure LinArith now named Lin_Arith
2009-03-13 haftmann 2009-03-13 moved some generic nonsense to arith_data.ML
2009-03-12 haftmann 2009-03-12 vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s