src/HOL/Hoare/HeapSyntax.thy

 
 subsection "Field access and update"
 
 syntax
   "_refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
-   (\<open>_/'((_ \<rightarrow> _)')\<close> [1000,0] 900)
+    (\<open>(\<open>open_block notation=\<open>mixfix Hoare ref update\<close>\<close>_/'((_ \<rightarrow> _)'))\<close> [1000,0] 900)
   "_fassign"  :: "'a ref => id => 'v => 's com"
-   (\<open>(2_^._ :=/ _)\<close> [70,1000,65] 61)
+    (\<open>(\<open>indent=2 notation=\<open>mixfix Hoare ref assignment\<close>\<close>_^._ :=/ _)\<close> [70,1000,65] 61)
   "_faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
-   (\<open>_^._\<close> [65,1000] 65)
+    (\<open>(\<open>open_block notation=\<open>infix Hoare ref access\<close>\<close>_^._)\<close> [65,1000] 65)
 translations
   "f(r \<rightarrow> v)" == "f(CONST addr r := v)"
   "p^.f := e" => "f := f(p \<rightarrow> e)"
   "p^.f" => "f(CONST addr p)"