diff -r b31c2132176a -r f4d76cb26433 src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Tue Jul 04 01:12:42 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy	Tue Jul 04 10:54:32 2000 +0200
@@ -48,6 +48,12 @@
   (* cf. 15.7.1 *)
   Lit				   "G\\<turnstile>Norm s -Lit v\\<succ>v\\<rightarrow> Norm s"
 
+  BinOp "\\<lbrakk>G\\<turnstile>Norm s -e1\\<succ>v1\\<rightarrow> s1;
+	  G\\<turnstile>s1     -e1\\<succ>v2\\<rightarrow> s2;
+	  v = (case bop of Eq  \\<Rightarrow> Bool (v1 = v2)
+	                 | Add \\<Rightarrow> Intg (the_Intg v1 + the_Intg v2))\\<rbrakk> \\<Longrightarrow>
+				   G\\<turnstile>Norm s -BinOp bop e1 e2\\<succ>v\\<rightarrow> s2"
+
   (* cf. 15.13.1, 15.2 *)
   LAcc				  "G\\<turnstile>Norm s -LAcc v\\<succ>the (locals s v)\\<rightarrow> Norm s"