--- a/src/HOL/NanoJava/State.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/NanoJava/State.thy Wed Feb 24 22:09:50 2010 +0100
@@ -84,9 +84,9 @@
lupd :: "vname => val => state => state" ("lupd'(_|->_')" [10,10] 1000)
"lupd x v s \<equiv> s (| locals := ((locals s)(x\<mapsto>v ))|)"
-syntax (xsymbols)
- hupd :: "loc => obj => state => state" ("hupd'(_\<mapsto>_')" [10,10] 1000)
- lupd :: "vname => val => state => state" ("lupd'(_\<mapsto>_')" [10,10] 1000)
+notation (xsymbols)
+ hupd ("hupd'(_\<mapsto>_')" [10,10] 1000) and
+ lupd ("lupd'(_\<mapsto>_')" [10,10] 1000)
constdefs