src/HOL/Fields.thy
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-27 hoelzl 2013-08-27 renamed typeclass dense_linorder to unbounded_dense_linorder
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2011-09-13 huffman 2011-09-13 tuned proofs
2011-09-03 huffman 2011-09-03 simplify proof
2011-08-08 huffman 2011-08-08 moved division ring stuff from Rings.thy to Fields.thy
2011-05-20 hoelzl 2011-05-20 add divide_.._cancel, inverse_.._iff
2010-05-08 huffman 2010-05-08 add lemmas one_less_inverse and one_le_inverse
2010-05-06 haftmann 2010-05-06 moved some lemmas from Groebner_Basis here
2010-04-27 haftmann 2010-04-27 tuned whitespace
2010-04-27 haftmann 2010-04-27 got rid of [simplified]
2010-04-27 haftmann 2010-04-27 tuned class linordered_field_inverse_zero
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
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-25 haftmann 2010-04-25 field_simps as named theorems
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-04 hoelzl 2010-03-04 Add dense_le, dense_le_bounded, field_le_mult_one_interval.
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2010-02-10 haftmann 2010-02-10 moved lemma field_le_epsilon from Real.thy to Fields.thy
2010-02-10 haftmann 2010-02-10 moved constants inverse and divide to Ring.thy
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields