--- a/IntEx.thy	Tue Oct 27 09:01:12 2009 +0100
+++ b/IntEx.thy	Tue Oct 27 11:03:38 2009 +0100
@@ -110,13 +110,21 @@
 where
  "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
 
+lemma plus_sym_pre:
+  shows "intrel (my_plus a b) (my_plus b a)"
+  apply(cases a)
+  apply(cases b)
+  apply(auto)
+  done
+
 lemma equiv_intrel: "EQUIV intrel"
   sorry
 
 lemma intrel_refl: "intrel a a"
   sorry
 
-lemma ho_plus_rsp : "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus"
+lemma ho_plus_rsp : 
+  "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus"
   by (simp)
 
 ML {* val consts = [@{const_name "my_plus"}] *}