src/HOL/Rings.thy
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Tue, 13 Sep 2011 17:07:33 -0700 huffman tuned proofs
Sat, 20 Aug 2011 15:19:35 -0700 huffman replace lemma realpow_two_diff with new lemma square_diff_square_factored
Sat, 20 Aug 2011 10:08:47 -0700 huffman rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
Mon, 08 Aug 2011 09:52:09 -0700 huffman moved division ring stuff from Rings.thy to Fields.thy
Mon, 23 Aug 2010 11:17:13 +0200 haftmann dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s
Mon, 17 May 2010 18:59:59 -0700 huffman declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
Mon, 17 May 2010 08:45:46 -0700 huffman remove simp attribute from square_eq_1_iff
Mon, 10 May 2010 21:27:52 -0700 huffman move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
Thu, 06 May 2010 23:11:56 +0200 haftmann moved some lemmas from Groebner_Basis here
Tue, 20 Apr 2010 17:58:34 +0200 hoelzl Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
Mon, 26 Apr 2010 11:34:15 +0200 haftmann dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
Fri, 23 Apr 2010 15:17:59 +0200 haftmann less special treatment of times_divide_eq [simp]
Fri, 23 Apr 2010 13:58:14 +0200 haftmann more localization; factored out lemmas for division_ring
Thu, 18 Mar 2010 12:58:52 +0100 blanchet now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
Sat, 06 Mar 2010 18:24:30 -0800 huffman generalize some lemmas from class linordered_ring_strict to linordered_ring
Mon, 22 Feb 2010 15:53:18 +0100 haftmann tuned text
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Wed, 10 Feb 2010 15:52:12 +0100 haftmann dropped last occurence of the linlinordered accident
Wed, 10 Feb 2010 14:12:04 +0100 haftmann moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
Wed, 10 Feb 2010 08:49:26 +0100 haftmann division ring assumes divide_inverse
Mon, 08 Feb 2010 17:12:38 +0100 haftmann renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
less more (0) tip