| 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