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 \ int"} *}