--- a/src/HOL/Auth/NS_Shared.thy Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Wed May 12 16:44:49 2010 +0200
@@ -14,15 +14,14 @@
Proc. Royal Soc. 426
*}
-constdefs
-
+definition
(* 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] => bool"
- ("_ Issues _ with _ on _")
- "A Issues B with X on evs ==
- \<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
- X \<notin> parts (spies (takeWhile (% z. z \<noteq> Says A B Y) (rev evs)))"
+ ("_ Issues _ with _ on _") where
+ "A Issues B with X on evs =
+ (\<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
+ X \<notin> parts (spies (takeWhile (% z. z \<noteq> Says A B Y) (rev evs))))"
inductive_set ns_shared :: "event list set"