src/HOL/Nat_Numeral.thy
Sat, 20 Aug 2011 09:59:28 -0700 huffman add lemma power2_eq_iff
Thu, 23 Jun 2011 09:04:20 -0700 huffman added number_semiring class, plus a few new lemmas;
Wed, 22 Jun 2011 15:58:55 -0700 huffman generalize lemmas power_number_of_even and power_number_of_odd
Thu, 25 Nov 2010 00:17:16 +0100 blanchet added "no_atp" for fact that confuses the SMT normalizer and that doesn't help ATPs anyway
Sun, 24 Oct 2010 20:19:00 +0200 nipkow nat_number -> eval_nat_numeral
Mon, 17 May 2010 08:40:17 -0700 huffman remove simp attribute from power2_eq_1_iff
Tue, 11 May 2010 19:01:35 -0700 huffman include iszero_simps in semiring_norm just once (they are already included in rel_simps)
Tue, 11 May 2010 06:27:06 -0700 huffman add lemma power2_eq_1_iff; generalize some other lemmas
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
Wed, 05 May 2010 16:53:21 +0200 haftmann moved nat_arith ot Nat_Numeral: clarified normalizer setup
Wed, 17 Mar 2010 19:55:07 +0100 boehmes tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
Sat, 06 Mar 2010 18:24:30 -0800 huffman generalize some lemmas from class linordered_ring_strict to linordered_ring
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Mon, 08 Feb 2010 17:12:27 +0100 haftmann hide fact Nat.add_0_right; make add_0_right from Groups priority
Mon, 08 Feb 2010 14:22:22 +0100 haftmann dropped accidental duplication of "lin" prefix from cs. 108662d50512
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Thu, 29 Oct 2009 22:16:12 +0100 haftmann moved some lemmas to theory Int
Wed, 28 Oct 2009 19:09:47 +0100 haftmann moved theory Divides after theory Nat_Numeral; tuned some proof texts
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
Wed, 24 Jun 2009 09:41:14 +0200 nipkow corrected and unified thm names
Fri, 15 May 2009 16:39:18 +0200 haftmann tuned code postprocessor
Mon, 11 May 2009 19:51:21 +0200 haftmann merged
Mon, 11 May 2009 15:18:32 +0200 haftmann tuned interface of Lin_Arith
Mon, 11 May 2009 08:28:49 -0700 huffman newline at end of file
Sat, 09 May 2009 07:25:22 +0200 nipkow lemmas by Andreas Lochbihler
Fri, 08 May 2009 09:48:07 +0200 haftmann modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
Mon, 04 May 2009 14:49:49 +0200 haftmann dropped duplicate lemma sum_nonneg_eq_zero_iff
Tue, 28 Apr 2009 15:50:29 +0200 haftmann collected square lemmas in Nat_Numeral
Mon, 27 Apr 2009 10:11:46 +0200 haftmann whitespace tuning
Wed, 22 Apr 2009 19:09:21 +0200 haftmann power operation defined generic
Wed, 15 Apr 2009 15:30:39 +0200 haftmann theory NatBin now named Nat_Numeral
less more (0) tip