1.1 --- a/src/HOL/Auth/Event.thy	Fri Mar 02 13:26:55 2001 +0100
     1.2 +++ b/src/HOL/Auth/Event.thy	Mon Mar 05 12:31:31 2001 +0100
     1.3 @@ -37,8 +37,8 @@
     1.4  
     1.5  axioms
     1.6    (*Spy has access to his own key for spoof messages, but Server is secure*)
     1.7 -  Spy_in_bad     [iff] :     "Spy: bad"
     1.8 -  Server_not_bad [iff] : "Server ~: bad"
     1.9 +  Spy_in_bad     [iff] :    "Spy \<in> bad"
    1.10 +  Server_not_bad [iff] : "Server \<notin> bad"
    1.11  
    1.12  primrec
    1.13    knows_Nil:   "knows A [] = initState A"
    1.14 @@ -49,7 +49,7 @@
    1.15  	   Says A' B X => insert X (knows Spy evs)
    1.16  	 | Gets A' X => knows Spy evs
    1.17  	 | Notes A' X  => 
    1.18 -	     if A' : bad then insert X (knows Spy evs) else knows Spy evs)
    1.19 +	     if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
    1.20  	else
    1.21  	(case ev of
    1.22  	   Says A' B X => 
    1.23 @@ -84,6 +84,6 @@
    1.24  method_setup analz_mono_contra = {*
    1.25      Method.no_args
    1.26        (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
    1.27 -    "for proving theorems of the form X ~: analz (knows Spy evs) --> P"
    1.28 +    "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
    1.29  
    1.30  end

     2.1 --- a/src/HOL/Auth/Message.thy	Fri Mar 02 13:26:55 2001 +0100
     2.2 +++ b/src/HOL/Auth/Message.thy	Mon Mar 05 12:31:31 2001 +0100
     2.3 @@ -11,7 +11,7 @@
     2.4  files ("Message_lemmas.ML"):
     2.5  
     2.6  (*Eliminates a commonly-occurring expression*)
     2.7 -lemma [simp] : "~ (ALL x. x~=y)"
     2.8 +lemma [simp] : "~ (\<forall> x. x\<noteq>y)"
     2.9  by blast
    2.10  
    2.11  (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
    2.12 @@ -66,17 +66,17 @@
    2.13  
    2.14    (*Keys useful to decrypt elements of a message set*)
    2.15    keysFor :: "msg set => key set"
    2.16 -  "keysFor H == invKey ` {K. EX X. Crypt K X : H}"
    2.17 +  "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
    2.18  
    2.19  (** Inductive definition of all "parts" of a message.  **)
    2.20  
    2.21  consts  parts   :: "msg set => msg set"
    2.22  inductive "parts H"
    2.23    intros 
    2.24 -    Inj [intro]          : "X: H  ==> X : parts H"
    2.25 -    Fst:     "{|X,Y|}   : parts H ==> X : parts H"
    2.26 -    Snd:     "{|X,Y|}   : parts H ==> Y : parts H"
    2.27 -    Body:    "Crypt K X : parts H ==> X : parts H"
    2.28 +    Inj [intro]:               "X \<in> H ==> X \<in> parts H"
    2.29 +    Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
    2.30 +    Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
    2.31 +    Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
    2.32  
    2.33  
    2.34  (*Monotonicity*)
    2.35 @@ -94,11 +94,11 @@
    2.36  consts  analz   :: "msg set => msg set"
    2.37  inductive "analz H"
    2.38    intros 
    2.39 -    Inj [intro,simp] :    "X: H ==> X: analz H"
    2.40 -    Fst:     "{|X,Y|} : analz H ==> X : analz H"
    2.41 -    Snd:     "{|X,Y|} : analz H ==> Y : analz H"
    2.42 +    Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
    2.43 +    Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
    2.44 +    Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
    2.45      Decrypt [dest]: 
    2.46 -             "[|Crypt K X : analz H; Key(invKey K): analz H|] ==> X : analz H"
    2.47 +             "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
    2.48  
    2.49  
    2.50  (*Monotonicity; Lemma 1 of Lowe's paper*)
    2.51 @@ -116,12 +116,12 @@
    2.52  consts  synth   :: "msg set => msg set"
    2.53  inductive "synth H"
    2.54    intros 
    2.55 -    Inj    [intro]:   "X: H ==> X: synth H"
    2.56 -    Agent  [intro]:   "Agent agt : synth H"
    2.57 -    Number [intro]:   "Number n  : synth H"
    2.58 -    Hash   [intro]:   "X: synth H ==> Hash X : synth H"
    2.59 -    MPair  [intro]:   "[|X: synth H;  Y: synth H|] ==> {|X,Y|} : synth H"
    2.60 -    Crypt  [intro]:   "[|X: synth H;  Key(K) : H|] ==> Crypt K X : synth H"
    2.61 +    Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
    2.62 +    Agent  [intro]:   "Agent agt \<in> synth H"
    2.63 +    Number [intro]:   "Number n  \<in> synth H"
    2.64 +    Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
    2.65 +    MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
    2.66 +    Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
    2.67  
    2.68  (*Monotonicity*)
    2.69  lemma synth_mono: "G<=H ==> synth(G) <= synth(H)"
    2.70 @@ -131,11 +131,11 @@
    2.71  done
    2.72  
    2.73  (*NO Agent_synth, as any Agent name can be synthesized.  Ditto for Number*)
    2.74 -inductive_cases Nonce_synth [elim!]: "Nonce n : synth H"
    2.75 -inductive_cases Key_synth   [elim!]: "Key K : synth H"
    2.76 -inductive_cases Hash_synth  [elim!]: "Hash X : synth H"
    2.77 -inductive_cases MPair_synth [elim!]: "{|X,Y|} : synth H"
    2.78 -inductive_cases Crypt_synth [elim!]: "Crypt K X : synth H"
    2.79 +inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
    2.80 +inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
    2.81 +inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
    2.82 +inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
    2.83 +inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
    2.84  
    2.85  use "Message_lemmas.ML"
    2.86