src/HOL/Quotient_Examples/Quotient_Int.thy
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