--- a/IntEx.thy	Tue Oct 27 12:20:57 2009 +0100
+++ b/IntEx.thy	Tue Oct 27 14:59:00 2009 +0100
@@ -3,7 +3,7 @@
 begin
 
 fun
-  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" 
+  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
 where
   "intrel (x, y) (u, v) = (x + v = u + y)"
 
@@ -123,7 +123,7 @@
 lemma intrel_refl: "intrel a a"
   sorry
 
-lemma ho_plus_rsp : 
+lemma ho_plus_rsp:
   "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus"
   by (simp)