# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256637818 -3600
# Node ID d6bf4234c7f63927a723a3daa6a2e4e126d7a053
# Parent  ff4425e000dbde596e31537a2dc7392e887265e4
merged

diff -r ff4425e000db -r d6bf4234c7f6 IntEx.thy
--- 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"}] *}