
diff -r 37f7dc85b61b -r 3d7a9d4d2bb6 Quot/Examples/IntEx2.thy
--- 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"} *}




