src/HOL/Auth/KerberosIV.thy
changeset 13507 febb8e5d2a9d
parent 11704 3c50a2cd6f00
child 14182 5f49f00fe084
     1.1 --- a/src/HOL/Auth/KerberosIV.thy	Fri Aug 16 17:19:43 2002 +0200
     1.2 +++ b/src/HOL/Auth/KerberosIV.thy	Sat Aug 17 14:55:08 2002 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4                        
     1.5   (* A is the true creator of X if she has sent X and X never appeared on
     1.6      the trace before this event. Recall that traces grow from head. *)
     1.7 -  Issues :: [agent , agent, msg, event list] => bool ("_ Issues _ with _ on _")
     1.8 +  Issues :: [agent, agent, msg, event list] => bool ("_ Issues _ with _ on _")
     1.9     "A Issues B with X on evs == 
    1.10        \\<exists>Y. Says A B Y \\<in> set evs & X \\<in> parts {Y} &
    1.11        X \\<notin> parts (spies (takeWhile (% z. z  \\<noteq> Says A B Y) (rev evs)))"