2009-02-23 huffman 2009-02-23 make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
2008-12-06 huffman 2008-12-06 change lemmas to avoid using neg
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-09-29 haftmann 2008-09-29 clarified dependencies between arith tools
2008-03-28 wenzelm 2008-03-28 avoid rebinding of existing facts;
2008-03-18 wenzelm 2008-03-18 avoid rebinding of existing facts;
2008-02-27 chaieb 2008-02-27 Installation of Quantifier elimination for ordered fields moved to Library/Dense_Linear_Order.thy
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2007-11-28 haftmann 2007-11-28 dropped legacy ml bindings
2007-10-31 chaieb 2007-10-31 exported field_comp_conv: a numerical conversion over fields
2007-10-21 chaieb 2007-10-21 Fixed Bug in instantiation of Groebner Bases to field: dest_const used to raise TERM where the tactic handles ERROR
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-07-31 wenzelm 2007-07-31 arith method setup: proper context;
2007-07-22 chaieb 2007-07-22 Tunes Proof
2007-07-20 haftmann 2007-07-20 moved class ord from Orderings.thy to HOL.thy
2007-07-05 wenzelm 2007-07-05 Numeral.mk_cnumber;
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-06-21 wenzelm 2007-06-21 moved Presburger setup back to Presburger.thy;
2007-06-21 wenzelm 2007-06-21 renamed NatSimprocs.thy to Arith_Tools.thy; incorporated HOL/Presburger.thy into NatSimprocs.thy;