Add output translation for <a := .., b := .., ..> state notation.
authorkleing
Thu Nov 07 16:08:19 2013 +1100 (2013-11-07)
changeset 542895a1be63f32cf
parent 54288 ce58fb149ff6
child 54290 fee1276d47f7
Add output translation for <a := .., b := .., ..> state notation.
src/HOL/IMP/AExp.thy
     1.1 --- a/src/HOL/IMP/AExp.thy	Thu Nov 07 02:42:20 2013 +0100
     1.2 +++ b/src/HOL/IMP/AExp.thy	Thu Nov 07 16:08:19 2013 +1100
     1.3 @@ -33,6 +33,7 @@
     1.4    "_State" :: "updbinds => 'a" ("<_>")
     1.5  translations
     1.6    "_State ms" == "_Update <> ms"
     1.7 +  "_State (_updbinds b bs)" <= "_Update (_State b) bs"
     1.8  
     1.9  text {* \noindent
    1.10    We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly: