src/HOL/Auth/Event.thy
changeset 13956 8fe7e12290e1
parent 13935 4822d9597d1e
child 14126 28824746d046
     1.1 --- a/src/HOL/Auth/Event.thy	Mon May 05 15:55:56 2003 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Mon May 05 18:22:01 2003 +0200
     1.3 @@ -3,14 +3,14 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1996  University of Cambridge
     1.6  
     1.7 -Theory of events for security protocols
     1.8 -
     1.9  Datatype of events; function "spies"; freshness
    1.10  
    1.11  "bad" agents have been broken by the Spy; their private keys and internal
    1.12      stores are visible to him
    1.13  *)
    1.14  
    1.15 +header{*Theory of Events for Security Protocols*}
    1.16 +
    1.17  theory Event = Message:
    1.18  
    1.19  consts  (*Initial states of agents -- parameter of the construction*)
    1.20 @@ -99,10 +99,9 @@
    1.21  
    1.22  subsection{*Function @{term knows}*}
    1.23  
    1.24 -text{*Simplifying   @term{"parts (insert X (knows Spy evs))
    1.25 -      = parts {X} \<union> parts (knows Spy evs)"}.  The general case loops.*)
    1.26 -
    1.27 -text{*This version won't loop with the simplifier.*}
    1.28 +(*Simplifying   
    1.29 + parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
    1.30 +  This version won't loop with the simplifier.*)
    1.31  lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
    1.32  
    1.33  lemma knows_Spy_Says [simp]: