src/HOL/Rings.thy
2014-09-07 haftmann 2014-09-07 generalized
2014-09-06 haftmann 2014-09-06 added various facts
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-04-12 nipkow 2014-04-12 made mult_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-04-09 hoelzl 2014-04-09 field_simps: better support for negation and division, and power
2014-03-19 paulson 2014-03-19 Some rationalisation of basic lemmas
2014-03-04 huffman 2014-03-04 fix typo
2014-01-30 haftmann 2014-01-30 split rules for of_bool, similar to if
2013-12-09 wenzelm 2013-12-09 more antiquotations;
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-04 haftmann 2013-11-04 fact generalization and name consolidation
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-10-31 haftmann 2013-10-31 generalized of_bool conversion
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-03-26 hoelzl 2013-03-26 move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
2012-12-07 nipkow 2012-12-07 corrected nonsensical associativity of `` and dvd
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
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