diff -r d0250d01782c -r df053507edba Quot/Examples/IntEx.thy --- a/Quot/Examples/IntEx.thy Sun Dec 20 00:15:40 2009 +0100 +++ b/Quot/Examples/IntEx.thy Sun Dec 20 00:26:53 2009 +0100 @@ -7,7 +7,7 @@ where "intrel (x, y) (u, v) = (x + v = u + y)" -quotient my_int = "nat \ nat" / intrel +quotient_type my_int = "nat \ nat" / intrel apply(unfold equivp_def) apply(auto simp add: mem_def expand_fun_eq) done