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