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/Separation.thy
changeset 81189 47a0dfee26ea
parent 80914 d97fdabd9e2b 
--- a/src/HOL/Hoare/Separation.thy	Fri Oct 18 16:31:35 2024 +0200
+++ b/src/HOL/Hoare/Separation.thy	Fri Oct 18 16:37:39 2024 +0200
@@ -52,9 +52,15 @@
 
 syntax
  "_emp" :: "bool" (\<open>emp\<close>)
- "_singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" (\<open>[_ \<mapsto> _]\<close>)
- "_star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl \<open>**\<close> 60)
- "_wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl \<open>-*\<close> 60)
+ "_singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool"  (\<open>(\<open>open_block notation=\<open>mixfix singl\<close>\<close>[_ \<mapsto> _])\<close>)
+ "_star" :: "bool \<Rightarrow> bool \<Rightarrow> bool"  (infixl \<open>**\<close> 60)
+ "_wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool"  (infixl \<open>-*\<close> 60)
+
+syntax_consts
+  "_emp" \<rightleftharpoons> is_empty and
+  "_singl" \<rightleftharpoons> singl and
+  "_star" \<rightleftharpoons> star and
+  "_wand" \<rightleftharpoons> wand
 
 (* FIXME does not handle "_idtdummy" *)
 ML \<open>
isabelle