src/HOL/IMP/AExp.thy

--- a/src/HOL/IMP/AExp.thy	Thu Nov 07 02:42:20 2013 +0100
+++ b/src/HOL/IMP/AExp.thy	Thu Nov 07 16:08:19 2013 +1100
@@ -33,6 +33,7 @@
   "_State" :: "updbinds => 'a" ("<_>")
 translations
   "_State ms" == "_Update <> ms"
+  "_State (_updbinds b bs)" <= "_Update (_State b) bs"
 
 text {* \noindent
   We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly: