# HG changeset patch
# User kleing
# Date 1383800899 -39600
# Node ID 5a1be63f32cf5706ffb0d3d4d3b0f3e3cf7f8977
# Parent  ce58fb149ff674924c85472f821ec3b89706294f
Add output translation for <a := .., b := .., ..> state notation.

diff -r ce58fb149ff6 -r 5a1be63f32cf 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: