src/HOL/MicroJava/J/Term.thy
changeset 10042 7164dc0d24d8
parent 9348 f495dba0cb07
child 10061 fe82134773dc
     1.1 --- a/src/HOL/MicroJava/J/Term.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/Term.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  	| Lit	val		   (* literal value, also references *)
     1.5          | BinOp binop  expr expr   (* binary operation *)
     1.6  	| LAcc vname		   (* local (incl. parameter) access *)
     1.7 -	| LAss vname expr          (* local assign *) ("_\\<Colon>=_"  [      90,90]90)
     1.8 +	| LAss vname expr          (* local assign *) ("_::=_"  [      90,90]90)
     1.9  	| FAcc cname expr vname    (* field access *) ("{_}_.._"[10,90,99   ]90)
    1.10  	| FAss cname expr vname 
    1.11  	                  expr     (* field ass. *)("{_}_.._:=_"[10,90,99,90]90)