src/HOL/Decision_Procs/Rat_Pair.thy
10 months ago nipkow 2018-06-14 tuned
16 months ago wenzelm 2017-12-03 misc tuning and modernization;
17 months ago haftmann 2017-11-11 dedicated definition for coprimality
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2015-07-09 wenzelm 2015-07-09 tuned proofs;
2015-06-24 wenzelm 2015-06-24 tuned proofs -- less digits;
2015-06-20 wenzelm 2015-06-20 tuned proofs;
2015-06-20 wenzelm 2015-06-20 isabelle update_cartouches;
2015-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2014-11-17 haftmann 2014-11-17 formally self-contained gcd type classes
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-30 haftmann 2014-10-30 more simp rules concerning dvd and even/odd
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-09 hoelzl 2014-04-09 revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
2014-04-04 paulson 2014-04-04 divide_minus_left divide_minus_right are in field_simps but are not default simprules
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-10-31 haftmann 2013-10-31 more convenient place for a theory in solitariness