src/HOL/IMP/VC.thy

   vcawp :: "acom => assn => assn * assn"
   astrip :: acom => com
 
 primrec awp acom
   "awp Askip Q = Q"
-  "awp (Aass x a) Q = (%s. Q(s[a s/x]))"
+  "awp (Aass x a) Q = (%s. Q(s[x:=a s]))"
   "awp (Asemi c d) Q = awp c (awp d Q)"
   "awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))" 
   "awp (Awhile b I c) Q = I"
 
 primrec vc acom

   "astrip (Awhile b I c) = (WHILE b DO astrip c)"
 
 (* simultaneous computation of vc and awp: *)
 primrec vcawp acom
   "vcawp Askip Q = (%s. True, Q)"
-  "vcawp (Aass x a) Q = (%s. True, %s. Q(s[a s/x]))"
+  "vcawp (Aass x a) Q = (%s. True, %s. Q(s[x:=a s]))"
   "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
                               (vcc,wpc) = vcawp c wpd
                           in (%s. vcc s & vcd s, wpc))"
   "vcawp (Aif b c d) Q = (let (vcd,wpd) = vcawp d Q;
                               (vcc,wpc) = vcawp c Q