src/HOL/MicroJava/J/Term.thy
changeset 10061 fe82134773dc
parent 10042 7164dc0d24d8
child 10069 c7226e6f9625
     1.1 --- a/src/HOL/MicroJava/J/Term.thy	Fri Sep 22 16:28:04 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/Term.thy	Fri Sep 22 16:28:53 2000 +0200
     1.3 @@ -11,21 +11,23 @@
     1.4  datatype binop = Eq | Add	   (* function codes for binary operation *)
     1.5  
     1.6  datatype expr
     1.7 -	= NewC	cname		   (* class instance creation *)
     1.8 -	| Cast	cname expr	   (* type cast *)
     1.9 -	| Lit	val		   (* literal value, also references *)
    1.10 -        | BinOp binop  expr expr   (* binary operation *)
    1.11 -	| LAcc vname		   (* local (incl. parameter) access *)
    1.12 -	| LAss vname expr          (* local assign *) ("_::=_"  [      90,90]90)
    1.13 -	| FAcc cname expr vname    (* field access *) ("{_}_.._"[10,90,99   ]90)
    1.14 +	= NewC	cname              (* class instance creation *)
    1.15 +	| Cast	cname expr         (* type cast *)
    1.16 +	| Lit	val                  (* literal value, also references *)
    1.17 +  | BinOp binop  expr expr   (* binary operation *)
    1.18 +	| LAcc vname               (* local (incl. parameter) access *)
    1.19 +	| LAss vname expr          (* local assign *) ("_::=_"   [      90,90]90)
    1.20 +	| FAcc cname expr vname    (* field access *) ("{_}_.._" [10,90,99   ]90)
    1.21  	| FAss cname expr vname 
    1.22 -	                  expr     (* field ass. *)("{_}_.._:=_"[10,90,99,90]90)
    1.23 -	| Call expr mname (ty list) (expr list)(* method call*)
    1.24 -                                    ("_.._'({_}_')" [90,99,10,10] 90)
    1.25 +                    expr     (* field ass. *) ("{_}_.._:=_" [10,90,99,90]90)
    1.26 +	| Call expr mname 
    1.27 +    (ty list) (expr list)    (* method call*) ("_.._'({_}_')" [90,99,10,10] 90)
    1.28 +
    1.29  and stmt
    1.30 -	= Skip			   (* empty      statement *)
    1.31 -	| Expr expr		   (* expression statement *)
    1.32 -	| Comp stmt stmt	   ("_;; _"			[      61,60]60)
    1.33 -	| Cond expr stmt stmt      ("If'(_') _ Else _"		[   80,79,79]70)
    1.34 -	| Loop expr stmt	   ("While'(_') _"		[      80,79]70)
    1.35 +	= Skip                     (* empty statement *)
    1.36 +  | Expr expr                (* expression statement *)
    1.37 +  | Comp stmt stmt       ("_;; _"             [61,60]60)
    1.38 +  | Cond expr stmt stmt  ("If '(_') _ Else _" [80,79,79]70)
    1.39 +  | Loop expr stmt       ("While '(_') _"     [80,79]70)
    1.40 +
    1.41  end