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_Typing.thy
changeset 69597 ff784d5a5bfb
parent 68776 403dd13cf6e9 
--- a/src/HOL/IMP/Sec_Typing.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/IMP/Sec_Typing.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -178,7 +178,7 @@
 
 subsubsection "The Standard Typing System"
 
-text\<open>The predicate @{prop"l \<turnstile> c"} is nicely intuitive and executable. The
+text\<open>The predicate \<^prop>\<open>l \<turnstile> c\<close> is nicely intuitive and executable. The
 standard formulation, however, is slightly different, replacing the maximum
 computation by an antimonotonicity rule. We introduce the standard system now
 and show the equivalence with our formulation.\<close>
isabelle