| changeset 61169 | 4de9ff3ea29a |
| parent 61076 | bdc1e2f0a86a |
| child 63167 | 0909deb8059b |
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Sun Sep 13 22:56:52 2015 +0200 @@ -188,8 +188,7 @@ "(sup :: int \<Rightarrow> int \<Rightarrow> int) = max" instance - by default - (auto simp add: inf_int_def sup_int_def max_min_distrib2) + by standard (auto simp add: inf_int_def sup_int_def max_min_distrib2) end