Quot/Examples/IntEx2.thy
changeset 715 3d7a9d4d2bb6
parent 711 810d59a3d9b0
child 719 a9e55e1ef64c
--- a/Quot/Examples/IntEx2.thy	Fri Dec 11 15:49:15 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Fri Dec 11 15:58:15 2009 +0100
@@ -15,7 +15,7 @@
   unfolding equivp_def
   by (auto simp add: mem_def expand_fun_eq)
 
-instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
+instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
 begin
 
 ML {* @{term "0 \<Colon> int"} *}