src/HOL/Int.thy
Mon, 16 Sep 2013 15:30:20 +0200 kuncar use lifting_forget for deregistering numeric types as a quotient type
Sun, 18 Aug 2013 15:29:50 +0200 haftmann added lemma
Sun, 23 Jun 2013 21:16:07 +0200 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
Wed, 15 May 2013 12:10:39 +0200 kuncar stronger reflexivity prover
Wed, 20 Feb 2013 12:04:42 +0100 hoelzl split dense into inner_dense_order and no_top/no_bot
Tue, 19 Feb 2013 15:03:36 +0100 kuncar delete also predicates on relations when hiding an implementation of an abstract type
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
Thu, 14 Feb 2013 12:24:42 +0100 haftmann abandoned theory Plain
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Sat, 02 Jun 2012 08:27:29 +0200 huffman transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
Wed, 30 May 2012 16:59:20 +0200 huffman convert Int.thy to use lifting and transfer
Wed, 30 May 2012 14:55:44 +0200 huffman remove unnecessary simp rules involving Abs_Integ
Sun, 01 Apr 2012 16:09:58 +0200 huffman removed Nat_Numeral.thy, moving all theorems elsewhere
Fri, 30 Mar 2012 16:44:23 +0200 huffman load Tools/numeral.ML in Num.thy
Fri, 30 Mar 2012 15:56:12 +0200 huffman set up numeral reorient simproc in Num.thy
Fri, 30 Mar 2012 08:10:28 +0200 huffman move lemmas from Nat_Numeral to Int.thy and Num.thy
Thu, 29 Mar 2012 14:09:10 +0200 huffman move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Fri, 02 Mar 2012 09:35:32 +0100 bulwahn adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
Thu, 29 Dec 2011 10:47:55 +0100 haftmann semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat; attribute code_abbrev superseedes code_unfold_post
Wed, 30 Nov 2011 16:27:10 +0100 wenzelm prefer typedef without extra definition and alternative name;
Sun, 20 Nov 2011 21:07:10 +0100 wenzelm eliminated obsolete "standard";
Thu, 17 Nov 2011 06:04:59 +0100 huffman simplify some proofs
Thu, 17 Nov 2011 06:01:47 +0100 huffman Int.thy: remove duplicate lemmas double_less_0_iff and odd_less_0, use {even,odd}_less_0_iff instead
Thu, 20 Oct 2011 17:27:14 +0200 huffman removed mult_Bit1 from int_arith_rules (cf. 882403378a41 and 3078fd2eec7b, where mult_num1 erroneously replaced mult_1)
Wed, 19 Oct 2011 15:42:43 +0200 wenzelm inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);
Wed, 19 Oct 2011 08:37:26 +0200 bulwahn removing old code generator setup for integers
Sun, 09 Oct 2011 11:13:53 +0200 huffman Int.thy: discontinued some legacy theorems
Sun, 04 Sep 2011 07:15:13 -0700 huffman introduce abbreviation 'int' earlier in Int.thy
Sun, 04 Sep 2011 06:27:59 -0700 huffman move lemmas nat_le_iff and nat_mono into Int.thy
Sat, 03 Sep 2011 16:00:09 -0700 huffman remove duplicate lemma nat_zero in favor of nat_0
Wed, 29 Jun 2011 18:12:34 +0200 wenzelm modernized some simproc setup;
Thu, 23 Jun 2011 09:04:20 -0700 huffman added number_semiring class, plus a few new lemmas;
Wed, 04 May 2011 15:37:39 +0200 wenzelm proper case_names for int_cases, int_of_nat_induct;
Tue, 19 Apr 2011 23:57:28 +0200 wenzelm eliminated Codegen.mode in favour of explicit argument;
Sun, 13 Mar 2011 22:55:50 +0100 wenzelm tuned headers;
Tue, 30 Nov 2010 15:58:09 +0100 haftmann adapted proofs to slightly changed definitions of congruent(2)
Fri, 01 Oct 2010 16:05:25 +0200 haftmann constant `contents` renamed to `the_elem`
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
less more (0) -100 -60 tip