--- 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)