src/HOL/IMP/VC.thy
changeset 45212 e87feee00a4c
parent 45015 fdac1e9880eb
child 45745 3a8bc5623410
--- a/src/HOL/IMP/VC.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/VC.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -8,7 +8,7 @@
 invariants. *}
 
 datatype acom = Askip
-              | Aassign name aexp
+              | Aassign vname aexp
               | Asemi   acom acom
               | Aif     bexp acom acom
               | Awhile  bexp assn acom