--- a/src/HOL/MicroJava/J/Term.thy Mon Sep 25 12:04:10 2000 +0200
+++ b/src/HOL/MicroJava/J/Term.thy Mon Sep 25 12:08:49 2000 +0200
@@ -8,23 +8,23 @@
Term = Value +
-datatype binop = Eq | Add (* function codes for binary operation *)
+datatype binop = Eq | Add (* function codes for binary operation *)
datatype expr
- = NewC cname (* class instance creation *)
- | Cast cname 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 *) ("_::=_" [ 90,90]90)
- | FAcc cname expr vname (* field access *) ("{_}_.._" [10,90,99 ]90)
- | FAss cname expr vname
+ = NewC cname (* class instance creation *)
+ | Cast cname 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 *) ("_::=_" [ 90,90]90)
+ | FAcc cname expr vname (* field access *) ("{_}_.._" [10,90,99 ]90)
+ | FAss cname expr vname
expr (* field ass. *) ("{_}_.._:=_" [10,90,99,90]90)
- | Call expr mname
+ | Call expr mname
(ty list) (expr list) (* method call*) ("_.._'({_}_')" [90,99,10,10] 90)
and stmt
- = Skip (* empty statement *)
+ = Skip (* empty statement *)
| Expr expr (* expression statement *)
| Comp stmt stmt ("_;; _" [61,60]60)
| Cond expr stmt stmt ("If '(_') _ Else _" [80,79,79]70)