| changeset 54863 | 82acc20ded73 |
| parent 49962 | a8cc904a6820 |
| child 57492 | 74bf65a1910a |
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Wed Dec 25 17:39:06 2013 +0100 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Wed Dec 25 17:39:06 2013 +0100 @@ -187,7 +187,7 @@ instance by default - (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1) + (auto simp add: inf_int_def sup_int_def max_min_distrib2) end