src/HOL/Library/Fraction_Field.thy
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-06-12 haftmann 2015-06-12 uniform _ div _ as infix syntax for ring division
2015-06-01 haftmann 2015-06-01 separate class for division operator, with particular syntax added in more specific classes
2015-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2014-11-02 wenzelm 2014-11-02 modernized header;
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
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-11-17 wenzelm 2013-11-17 tuned proofs;
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-25 wenzelm 2013-08-25 tuned proofs;
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-04-01 wenzelm 2012-04-01 more precise type annotation (cf. 6523a21076a8);
2012-02-21 wenzelm 2012-02-21 misc tuning; more indentation;
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2010-11-30 haftmann 2010-11-30 adaptions to changes in Equiv_Relation.thy
2010-11-29 haftmann 2010-11-29 equivI has replaced equiv.intro
2010-10-01 haftmann 2010-10-01 constant `contents` renamed to `the_elem`
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
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-24 huffman 2010-04-24 Library/Fraction_Field.thy: ordering relations for fractions
2010-04-23 haftmann 2010-04-23 separated instantiation of division_by_zero
2010-02-24 haftmann 2010-02-24 renamed theory Rational to Rat
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-06-23 chaieb 2009-06-23 Added Library/Fraction_Field.thy: The fraction field of any integral domain