src/HOL/Auth/Shared.thy
changeset 2012 1b234f1fd9c7
parent 1967 0ff58b41c037
child 2032 1bbf1bdcaf56
     1.1 --- a/src/HOL/Auth/Shared.thy	Mon Sep 23 18:19:02 1996 +0200
     1.2 +++ b/src/HOL/Auth/Shared.thy	Mon Sep 23 18:19:38 1996 +0200
     1.3 @@ -6,8 +6,6 @@
     1.4  Theory of Shared Keys (common to all symmetric-key protocols)
     1.5  
     1.6  Server keys; initial states of agents; new nonces and keys; function "sees" 
     1.7 -
     1.8 -IS THE Notes constructor needed??
     1.9  *)
    1.10  
    1.11  Shared = Message + List + 
    1.12 @@ -33,7 +31,6 @@
    1.13  
    1.14  datatype  (*Messages, and components of agent stores*)
    1.15    event = Says agent agent msg
    1.16 -        | Notes agent msg
    1.17  
    1.18  consts  
    1.19    sees1 :: [agent, event] => msg set
    1.20 @@ -43,7 +40,6 @@
    1.21               that is sent to it; it must note such things if/when received*)
    1.22    sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Enemy} then {X} else {})"
    1.23            (*part of A's internal state*)
    1.24 -  sees1_Notes "sees1 A (Notes A' X)   = (if A=A' then {X} else {})"
    1.25  
    1.26  consts  
    1.27    sees :: [agent, event list] => msg set