--- a/IntEx.thy	Tue Oct 27 11:03:38 2009 +0100
+++ b/IntEx.thy	Tue Oct 27 11:27:53 2009 +0100
@@ -144,13 +144,6 @@
   lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t
 *}
 
-lemma plus_sym_pre:
-  shows "intrel (my_plus a b) (my_plus b a)"
-  apply (cases a)
-  apply (cases b)
-  apply (simp)
-  done
-
 ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *}
 
 lemma plus_assoc_pre: