src/HOL/Library/Fraction_Field.thy
changeset 54863 82acc20ded73
parent 54463 faad28e65b48
child 57512 cc97b347b301
--- a/src/HOL/Library/Fraction_Field.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Library/Fraction_Field.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -424,7 +424,7 @@
 instance
   by intro_classes
     (auto simp add: abs_fract_def sgn_fract_def
-      min_max.sup_inf_distrib1 inf_fract_def sup_fract_def)
+      max_min_distrib2 inf_fract_def sup_fract_def)
 
 end