src/HOL/Int.thy
Fri, 27 Aug 2010 19:34:23 +0200 haftmann renamed class/constant eq to equal; tuned some instantiations
Mon, 19 Jul 2010 16:09:44 +0200 haftmann diff_minus subsumes diff_def
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s
Tue, 11 May 2010 08:36:02 +0200 haftmann renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution
Mon, 10 May 2010 14:55:04 +0200 haftmann moved int induction lemma to theory Int as int_bidirectional_induct
Fri, 07 May 2010 09:51:55 +0200 haftmann moved lemma zdvd_period to theory Int
Thu, 06 May 2010 23:11:56 +0200 haftmann moved some lemmas from Groebner_Basis here
Thu, 06 May 2010 18:16:07 +0200 haftmann moved generic lemmas to appropriate places
Tue, 27 Apr 2010 12:20:09 +0200 haftmann got rid of [simplified]
Mon, 26 Apr 2010 15:37:50 +0200 haftmann use new classes (linordered_)field_inverse_zero
Mon, 26 Apr 2010 11:34:17 +0200 haftmann class division_ring_inverse_zero
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
Tue, 06 Apr 2010 10:46:28 +0200 boehmes added missing mult_1_left to linarith simp rules
Thu, 18 Mar 2010 13:14:54 +0100 blanchet merged
Thu, 18 Mar 2010 12:58:52 +0100 blanchet now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
Wed, 17 Mar 2010 19:55:07 +0100 boehmes tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
Sun, 07 Mar 2010 08:40:38 -0800 huffman add more simp rules for Ints
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Sat, 13 Feb 2010 23:24:57 +0100 wenzelm modernized structures;
Mon, 08 Feb 2010 17:12:38 +0100 haftmann renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
Mon, 08 Feb 2010 14:06:41 +0100 haftmann separate library theory for type classes combining lattices with various algebraic structures
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Thu, 10 Dec 2009 17:34:18 +0000 paulson streamlined proofs
Fri, 13 Nov 2009 14:14:04 +0100 nipkow renamed lemmas "anti_sym" -> "antisym"
Sun, 08 Nov 2009 19:15:37 +0100 wenzelm modernized structure Reorient_Proc;
Fri, 30 Oct 2009 18:32:40 +0100 haftmann tuned code setup
Thu, 29 Oct 2009 22:13:11 +0100 haftmann moved some dvd [int] facts to Int
Thu, 29 Oct 2009 11:41:38 +0100 haftmann moved some dvd [int] facts to Int
Wed, 28 Oct 2009 19:09:47 +0100 haftmann moved theory Divides after theory Nat_Numeral; tuned some proof texts
Wed, 21 Oct 2009 17:34:35 +0200 blanchet renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
Fri, 28 Aug 2009 19:15:59 +0200 nipkow tuned proofs
Wed, 29 Jul 2009 16:42:47 +0200 haftmann added numeral code postprocessor rules on type int
Tue, 14 Jul 2009 16:27:32 +0200 haftmann prefer code_inline over code_unfold; use code_unfold_post where appropriate
Tue, 14 Jul 2009 10:54:04 +0200 haftmann code attributes use common underscore convention
Mon, 11 May 2009 15:18:32 +0200 haftmann tuned interface of Lin_Arith
Fri, 08 May 2009 09:48:07 +0200 haftmann modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
Fri, 08 May 2009 08:00:11 +0200 haftmann moved int_factor_simprocs.ML to theory Int
Wed, 29 Apr 2009 17:15:01 -0700 huffman reimplement reorientation simproc using theory data
Wed, 29 Apr 2009 14:20:26 +0200 haftmann farewell to class recpower
Tue, 28 Apr 2009 15:50:29 +0200 haftmann reorganization of power lemmas
Tue, 28 Apr 2009 13:34:46 +0200 haftmann local syntax for Ints; ephermal re-globalization
Mon, 27 Apr 2009 10:11:44 +0200 haftmann cleaned up theory power further
Wed, 22 Apr 2009 19:09:21 +0200 haftmann power operation defined generic
Wed, 01 Apr 2009 22:29:10 +0200 nipkow cleaned up setprod_zero-related lemmas
Wed, 01 Apr 2009 16:55:31 +0200 nipkow added setsum_pos_nat
Mon, 30 Mar 2009 12:07:59 -0700 huffman simplify theorem references
Mon, 30 Mar 2009 10:47:41 -0700 huffman no longer delay loading of assoc_fold.ML
Sun, 22 Mar 2009 20:46:10 +0100 haftmann distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
Thu, 12 Mar 2009 18:01:26 +0100 haftmann vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
Wed, 04 Mar 2009 17:12:23 -0800 huffman declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Mon, 02 Mar 2009 16:53:55 +0100 nipkow name changes
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
Thu, 19 Feb 2009 18:16:19 -0800 huffman declare of_int_number_of_eq [simp]
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;
less more (0) -60 tip