src/HOL/Auth/KerberosIV.thy

--- a/src/HOL/Auth/KerberosIV.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Auth/KerberosIV.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -32,19 +32,19 @@
  (* 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 _" [50, 0, 0, 50] 50) where
+             (\<open>_ Issues _ with _ on _\<close> [50, 0, 0, 50] 50) 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))))"
 
 definition
  (* Yields the subtrace of a given trace from its beginning to a given event *)
-  before :: "[event, event list] \<Rightarrow> event list" ("before _ on _" [0, 50] 50)
+  before :: "[event, event list] \<Rightarrow> event list" (\<open>before _ on _\<close> [0, 50] 50)
   where "(before ev on evs) = takeWhile (\<lambda>z. z \<noteq> ev) (rev evs)"
 
 definition
  (* States than an event really appears only once on a trace *)
-  Unique :: "[event, event list] \<Rightarrow> bool" ("Unique _ on _" [0, 50] 50)
+  Unique :: "[event, event list] \<Rightarrow> bool" (\<open>Unique _ on _\<close> [0, 50] 50)
   where "(Unique ev on evs) = (ev \<notin> set (tl (dropWhile (\<lambda>z. z \<noteq> ev) evs)))"
 
 
@@ -95,7 +95,7 @@
   "expiredA T evs == authlife + T < CT evs"
 
 abbreviation
-  valid :: "[nat, nat] \<Rightarrow> bool" ("valid _ wrt _" [0, 50] 50) where
+  valid :: "[nat, nat] \<Rightarrow> bool" (\<open>valid _ wrt _\<close> [0, 50] 50) where
   "valid T1 wrt T2 == T1 \<le> replylife + T2"
 
 (*---------------------------------------------------------------------*)