Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Hoare/HeapSyntaxAbort.thy
changeset 81189 47a0dfee26ea
parent 80914 d97fdabd9e2b 
--- a/src/HOL/Hoare/HeapSyntaxAbort.thy	Fri Oct 18 16:31:35 2024 +0200
+++ b/src/HOL/Hoare/HeapSyntaxAbort.thy	Fri Oct 18 16:37:39 2024 +0200
@@ -21,11 +21,11 @@
 
 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
   "_refupdate f r v" == "f(CONST addr r := v)"
   "p^.f := e" => "(p \<noteq> CONST Null) \<rightarrow> (f := _refupdate f p e)"
isabelle