diff -r 8ca1150f34d0 -r 1e227c9ee915 IntEx.thy --- 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 \ nat) \ (nat \ nat) \ bool" + intrel :: "(nat \ nat) \ (nat \ nat) \ 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)