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