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/Doc/Tutorial/Protocol/Public.thy
changeset 69505 cc2d676d5395
parent 67613 ce654b0e6d69 
--- a/src/Doc/Tutorial/Protocol/Public.thy	Wed Dec 26 16:07:28 2018 +0100
+++ b/src/Doc/Tutorial/Protocol/Public.thy	Wed Dec 26 16:25:20 2018 +0100
@@ -12,10 +12,10 @@
 
 text \<open>
 The function
-@{text pubK} maps agents to their public keys.  The function
-@{text priK} maps agents to their private keys.  It is merely
+\<open>pubK\<close> maps agents to their public keys.  The function
+\<open>priK\<close> maps agents to their private keys.  It is merely
 an abbreviation (cf.\ \S\ref{sec:abbreviations}) defined in terms of
-@{text invKey} and @{text pubK}.
+\<open>invKey\<close> and \<open>pubK\<close>.
 \<close>
 
 consts pubK :: "agent \<Rightarrow> key"
@@ -39,7 +39,7 @@
 
 text \<open>
 \noindent
-The set @{text bad} consists of those agents whose private keys are known to
+The set \<open>bad\<close> consists of those agents whose private keys are known to
 the spy.
 
 Two axioms are asserted about the public-key cryptosystem.
isabelle