| changeset 67443 | 3abf6a722518 | 
| parent 61956 | 38b73f7940af | 
| child 69597 | ff784d5a5bfb | 
--- a/src/HOL/Auth/ZhouGollmann.thy Tue Jan 16 09:12:16 2018 +0100 +++ b/src/HOL/Auth/ZhouGollmann.thy Tue Jan 16 09:30:00 2018 +0100 @@ -21,7 +21,7 @@ definition broken :: "agent set" where - \<comment>\<open>the compromised honest agents; TTP is included as it's not allowed to + \<comment> \<open>the compromised honest agents; TTP is included as it's not allowed to use the protocol\<close> "broken == bad - {Spy}"