src/HOL/Auth/Event.thy
changeset 11310 51e70b7bc315
parent 11192 5fd02b905a9a
child 11463 96b5b27da55c
     1.1 --- a/src/HOL/Auth/Event.thy	Fri May 18 17:18:43 2001 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Sat May 19 12:19:23 2001 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4    knows  :: "agent => event list => msg set"
     1.5  
     1.6  
     1.7 -(*"spies" is retained for compability's sake*)
     1.8 +(*"spies" is retained for compatibility's sake*)
     1.9  syntax
    1.10    spies  :: "event list => msg set"
    1.11  
    1.12 @@ -37,8 +37,8 @@
    1.13  
    1.14  axioms
    1.15    (*Spy has access to his own key for spoof messages, but Server is secure*)
    1.16 -  Spy_in_bad     [iff] :    "Spy \<in> bad"
    1.17 -  Server_not_bad [iff] : "Server \<notin> bad"
    1.18 +  Spy_in_bad     [iff] :    "Spy \\<in> bad"
    1.19 +  Server_not_bad [iff] : "Server \\<notin> bad"
    1.20  
    1.21  primrec
    1.22    knows_Nil:   "knows A [] = initState A"
    1.23 @@ -49,7 +49,7 @@
    1.24  	   Says A' B X => insert X (knows Spy evs)
    1.25  	 | Gets A' X => knows Spy evs
    1.26  	 | Notes A' X  => 
    1.27 -	     if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
    1.28 +	     if A' \\<in> bad then insert X (knows Spy evs) else knows Spy evs)
    1.29  	else
    1.30  	(case ev of
    1.31  	   Says A' B X => 
    1.32 @@ -84,6 +84,6 @@
    1.33  method_setup analz_mono_contra = {*
    1.34      Method.no_args
    1.35        (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
    1.36 -    "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
    1.37 +    "for proving theorems of the form X \\<notin> analz (knows Spy evs) --> P"
    1.38  
    1.39  end