src/HOL/MicroJava/J/Term.thy
changeset 10042 7164dc0d24d8
parent 9348 f495dba0cb07
child 10061 fe82134773dc
--- a/src/HOL/MicroJava/J/Term.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Term.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -16,7 +16,7 @@
 	| 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)
+	| 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)