src/HOL/Arith_Tools.thy
Mon, 23 Feb 2009 16:25:52 -0800 huffman 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
Sat, 06 Dec 2008 19:39:53 -0800 huffman change lemmas to avoid using neg
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
Mon, 29 Sep 2008 12:31:59 +0200 haftmann clarified dependencies between arith tools
Fri, 28 Mar 2008 19:43:54 +0100 wenzelm avoid rebinding of existing facts;
Tue, 18 Mar 2008 20:33:28 +0100 wenzelm avoid rebinding of existing facts;
Wed, 27 Feb 2008 14:39:48 +0100 chaieb Installation of Quantifier elimination for ordered fields moved to Library/Dense_Linear_Order.thy
Tue, 15 Jan 2008 16:19:23 +0100 haftmann joined theories IntDef, Numeral, IntArith to theory Int
Wed, 28 Nov 2007 09:01:34 +0100 haftmann dropped legacy ml bindings
Wed, 31 Oct 2007 12:19:33 +0100 chaieb exported field_comp_conv: a numerical conversion over fields
Sun, 21 Oct 2007 12:33:12 +0200 chaieb Fixed Bug in instantiation of Groebner Bases to field: dest_const used to raise TERM where the tactic handles ERROR
Wed, 15 Aug 2007 12:52:56 +0200 paulson ATP blacklisting is now in theory data, attribute noatp
Tue, 31 Jul 2007 00:56:26 +0200 wenzelm arith method setup: proper context;
Sun, 22 Jul 2007 17:53:42 +0200 chaieb Tunes Proof
Fri, 20 Jul 2007 14:28:25 +0200 haftmann moved class ord from Orderings.thy to HOL.thy
Thu, 05 Jul 2007 00:06:09 +0200 wenzelm Numeral.mk_cnumber;
Sat, 23 Jun 2007 19:33:22 +0200 nipkow tuned and renamed group_eq_simps and ring_eq_simps
Thu, 21 Jun 2007 20:48:47 +0200 wenzelm moved Presburger setup back to Presburger.thy;
Thu, 21 Jun 2007 17:28:50 +0200 wenzelm renamed NatSimprocs.thy to Arith_Tools.thy;
less more (0) tip