diff -r b31c2132176a -r f4d76cb26433 src/HOL/MicroJava/J/Term.thy
--- a/src/HOL/MicroJava/J/Term.thy	Tue Jul 04 01:12:42 2000 +0200
+++ b/src/HOL/MicroJava/J/Term.thy	Tue Jul 04 10:54:32 2000 +0200
@@ -21,10 +21,13 @@
 types	val = val_
 translations "val" <= (type) "val_"
 
+datatype binop = Eq | Add	   (* function codes for binary operation *)
+
 datatype expr
 	= NewC	cname		   (* class instance creation *)
 	| Cast	ty expr		   (* type cast *)
 	| Lit	val		   (* literal value, also references *)
+        | BinOp binop  expr expr   (* binary operation *)
 	| LAcc vname		   (* local (incl. parameter) access *)
 	| LAss vname expr          (* local assign *) ("_\\<Colon>=_"  [      90,90]90)
 	| FAcc cname expr vname    (* field access *) ("{_}_.._"[10,90,99   ]90)