changeset 13956 | 8fe7e12290e1 |
parent 13926 | 6e62e5357a10 |
child 14126 | 28824746d046 |
--- a/src/HOL/Auth/Message.thy Mon May 05 15:55:56 2003 +0200 +++ b/src/HOL/Auth/Message.thy Mon May 05 18:22:01 2003 +0200 @@ -7,6 +7,8 @@ Inductive relations "parts", "analz" and "synth" *) +header{*Theory of Agents and Messages for Security Protocols*} + theory Message = Main: (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)