src/HOL/Decision_Procs/Rat_Pair.thy
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