src/HOL/IMP/Denotation.thy

--- a/src/HOL/IMP/Denotation.thy	Tue May 05 17:28:22 1998 +0200
+++ b/src/HOL/IMP/Denotation.thy	Wed May 06 11:46:00 1998 +0200
@@ -20,7 +20,7 @@
 
 primrec C com
   C_skip    "C(SKIP) = id"
-  C_assign  "C(x := a) = {(s,t). t = s[a(s)/x]}"
+  C_assign  "C(x := a) = {(s,t). t = s[x:=a(s)]}"
   C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
   C_if      "C(IF b THEN c1 ELSE c2) = {(s,t). (s,t) : C(c1) & b(s)} Un
                                        {(s,t). (s,t) : C(c2) & ~ b(s)}"