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/Auth/KerberosV.thy
changeset 80914 d97fdabd9e2b
parent 76299 0ad6f6508274 
--- a/src/HOL/Auth/KerberosV.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Auth/KerberosV.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -33,7 +33,7 @@
  (* A is the true creator of X if she has sent X and X never appeared on
     the trace before this event. Recall that traces grow from head. *)
   Issues :: "[agent, agent, msg, event list] \<Rightarrow> bool"
-             ("_ Issues _ with _ on _") where
+             (\<open>_ Issues _ with _ on _\<close>) where
    "A Issues B with X on evs =
       (\<exists>Y. Says A B Y \<in> set evs \<and> X \<in> parts {Y} \<and>
         X \<notin> parts (spies (takeWhile (\<lambda>z. z  \<noteq> Says A B Y) (rev evs))))"
@@ -86,7 +86,7 @@
   "expiredA T evs == authlife + T < CT evs"
 
 abbreviation
-  valid :: "[nat, nat] \<Rightarrow> bool"  ("valid _ wrt _") where
+  valid :: "[nat, nat] \<Rightarrow> bool"  (\<open>valid _ wrt _\<close>) where
   "valid T1 wrt T2 == T1 \<le> replylife + T2"
 
 (*---------------------------------------------------------------------*)
isabelle