src/HOL/Int.thy
Mon, 16 Feb 2009 20:33:23 +0100 blanchet Added Nitpick tag to 'of_int_of_nat'.
Tue, 03 Feb 2009 11:16:28 +0100 krauss declare "nat o abs" as default measure for int
Sat, 31 Jan 2009 09:04:16 +0100 nipkow added some simp rules
Wed, 28 Jan 2009 16:57:12 +0100 nipkow merged - resolving conflics
Wed, 28 Jan 2009 16:29:16 +0100 nipkow Replaced group_ and ring_simps by algebra_simps;
Mon, 26 Jan 2009 22:14:18 +0100 haftmann stripped Id
Wed, 21 Jan 2009 23:40:23 +0100 haftmann no base sort in class import
Wed, 10 Dec 2008 12:31:35 -0800 huffman clean up diff_bin_simps
Tue, 09 Dec 2008 22:13:16 -0800 huffman move all neg-related lemmas to NatBin; make type of neg specific to int
Tue, 09 Dec 2008 20:36:20 -0800 huffman separate neg_simps from rel_simps
Thu, 04 Dec 2008 16:28:09 -0800 huffman revert to using eq_number_of_eq for simplification (Groebner_Examples.thy was broken)
Thu, 04 Dec 2008 12:32:38 -0800 huffman add named lemma lists: neg_simps and iszero_simps
Thu, 04 Dec 2008 11:14:24 -0800 huffman change arith_special simps to avoid using neg
Wed, 03 Dec 2008 21:50:36 -0800 huffman enable eq_bin_simps for simplifying equalities on numerals
Wed, 03 Dec 2008 20:45:42 -0800 huffman enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
Wed, 03 Dec 2008 14:23:03 -0800 huffman cleaned up subsection headings;
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
Mon, 10 Nov 2008 08:18:56 +0100 haftmann tuned
Wed, 22 Oct 2008 14:15:43 +0200 haftmann slightly tuned
Fri, 10 Oct 2008 06:45:53 +0200 haftmann `code func` now just `code`
Thu, 09 Oct 2008 08:47:27 +0200 haftmann established canonical argument order in SML code generators
Tue, 07 Oct 2008 16:07:18 +0200 haftmann tuned of_nat code generation
Thu, 25 Sep 2008 10:17:22 +0200 haftmann non left-linear equations for nbe
Fri, 25 Jul 2008 12:03:34 +0200 haftmann added class preorder
Mon, 30 Jun 2008 13:41:28 +0200 haftmann code generator setup for "int" also works under eta-contraction
Tue, 10 Jun 2008 15:30:56 +0200 haftmann removed some dubious code lemmas
Fri, 23 May 2008 16:41:39 +0200 berghofe Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
Fri, 25 Apr 2008 15:30:33 +0200 krauss Merged theories about wellfoundedness into one: Wellfounded.thy
Tue, 22 Apr 2008 08:33:16 +0200 haftmann constant HOL.eq now qualified
Wed, 02 Apr 2008 15:58:26 +0200 haftmann moved some code lemmas for Numerals here
Mon, 17 Mar 2008 18:37:00 +0100 wenzelm removed duplicate lemmas;
Sun, 17 Feb 2008 06:49:53 +0100 huffman New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
Sat, 16 Feb 2008 02:01:13 +0100 huffman added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
Fri, 15 Feb 2008 16:09:12 +0100 haftmann <= and < on nat no longer depend on wellfounded relations
Fri, 25 Jan 2008 14:53:52 +0100 haftmann moved definition of power on ints to theory Int
Mon, 21 Jan 2008 08:43:27 +0100 haftmann tuned code setup
Tue, 15 Jan 2008 16:19:23 +0100 haftmann joined theories IntDef, Numeral, IntArith to theory Int
less more (0) tip