--- a/IntEx.thy	Sat Nov 21 03:12:50 2009 +0100
+++ b/IntEx.thy	Sat Nov 21 10:58:08 2009 +0100
@@ -8,7 +8,6 @@
   "intrel (x, y) (u, v) = (x + v = u + y)"
 
 quotient my_int = "nat \<times> nat" / intrel
-  and    my_int' = "nat \<times> nat" / intrel
   apply(unfold EQUIV_def)
   apply(auto simp add: mem_def expand_fun_eq)
   done