src/HOL/Rings.thy
2011-09-13 huffman 2011-09-13 tuned proofs
2011-08-20 huffman 2011-08-20 replace lemma realpow_two_diff with new lemma square_diff_square_factored
2011-08-20 huffman 2011-08-20 rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
2011-08-08 huffman 2011-08-08 moved division ring stuff from Rings.thy to Fields.thy
2010-08-23 haftmann 2010-08-23 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-05-17 huffman 2010-05-17 declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
2010-05-17 huffman 2010-05-17 remove simp attribute from square_eq_1_iff
2010-05-10 huffman 2010-05-10 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
2010-05-06 haftmann 2010-05-06 moved some lemmas from Groebner_Basis here
2010-04-20 hoelzl 2010-04-20 Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
2010-04-23 haftmann 2010-04-23 less special treatment of times_divide_eq [simp]
2010-04-23 haftmann 2010-04-23 more localization; factored out lemmas for division_ring
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-06 huffman 2010-03-06 generalize some lemmas from class linordered_ring_strict to linordered_ring
2010-02-22 haftmann 2010-02-22 tuned text
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2010-02-10 haftmann 2010-02-10 dropped last occurence of the linlinordered accident
2010-02-10 haftmann 2010-02-10 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-02-10 haftmann 2010-02-10 division ring assumes divide_inverse
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields