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_Parallel/Quote_Antiquote.thy
changeset 80914 d97fdabd9e2b
parent 69597 ff784d5a5bfb 
--- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -3,9 +3,9 @@
 theory Quote_Antiquote imports Main begin
 
 syntax
-  "_quote"     :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"                ("(\<guillemotleft>_\<guillemotright>)" [0] 1000)
-  "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"                ("\<acute>_" [1000] 1000)
-  "_Assert"    :: "'a \<Rightarrow> 'a set"                    ("(\<lbrace>_\<rbrace>)" [0] 1000)
+  "_quote"     :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"                (\<open>(\<guillemotleft>_\<guillemotright>)\<close> [0] 1000)
+  "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"                (\<open>\<acute>_\<close> [1000] 1000)
+  "_Assert"    :: "'a \<Rightarrow> 'a set"                    (\<open>(\<lbrace>_\<rbrace>)\<close> [0] 1000)
 
 translations
   "\<lbrace>b\<rbrace>" \<rightharpoonup> "CONST Collect \<guillemotleft>b\<guillemotright>"
isabelle