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/IMP/Sec_TypingT.thy
changeset 80914 d97fdabd9e2b
parent 69597 ff784d5a5bfb 
--- a/src/HOL/IMP/Sec_TypingT.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/IMP/Sec_TypingT.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -5,7 +5,7 @@
 
 subsubsection "A Syntax Directed System"
 
-inductive sec_type :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile> _)" [0,0] 50) where
+inductive sec_type :: "nat \<Rightarrow> com \<Rightarrow> bool" (\<open>(_/ \<turnstile> _)\<close> [0,0] 50) where
 Skip:
   "l \<turnstile> SKIP"  |
 Assign:
@@ -172,7 +172,7 @@
 computation by an antimonotonicity rule. We introduce the standard system now
 and show the equivalence with our formulation.\<close>
 
-inductive sec_type' :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile>'' _)" [0,0] 50) where
+inductive sec_type' :: "nat \<Rightarrow> com \<Rightarrow> bool" (\<open>(_/ \<turnstile>'' _)\<close> [0,0] 50) where
 Skip':
   "l \<turnstile>' SKIP"  |
 Assign':
isabelle