Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add output translation for <a := .., b := .., ..> state notation.
authorkleing
Thu, 07 Nov 2013 16:08:19 +1100
changeset 54289 5a1be63f32cf
parent 54288 ce58fb149ff6
child 54290 fee1276d47f7
Add output translation for <a := .., b := .., ..> state notation.
src/HOL/IMP/AExp.thy file | annotate | diff | comparison | revisions 
--- 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:
isabelle