src/HOL/Quotient_Examples/Quotient_Rat.thy
2017-08-18 wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2016-10-18 haftmann 2016-10-18 suitable logical type class for abs, sgn
2016-10-16 haftmann 2016-10-16 more standardized names
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2015-02-19 haftmann 2015-02-19 establish unique preferred fact names
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-05-31 huffman 2012-05-31 temporarily comment out portion of Quotient_Examples/Quotient_Rat.thy, broken by changes to Int.thy
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-23 kuncar 2012-03-23 fix Quotient_Examples
2011-12-12 Cezary Kaliszyk 2011-12-12 Add Quotient_Rat: an example of using the quotient package with partial equivalence relations, defining rational numbers.