diff -r d9af64c26be6 -r 1b234f1fd9c7 src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Mon Sep 23 18:19:02 1996 +0200
+++ b/src/HOL/Auth/Shared.thy	Mon Sep 23 18:19:38 1996 +0200
@@ -6,8 +6,6 @@
 Theory of Shared Keys (common to all symmetric-key protocols)
 
 Server keys; initial states of agents; new nonces and keys; function "sees" 
-
-IS THE Notes constructor needed??
 *)
 
 Shared = Message + List + 
@@ -33,7 +31,6 @@
 
 datatype  (*Messages, and components of agent stores*)
   event = Says agent agent msg
-        | Notes agent msg
 
 consts  
   sees1 :: [agent, event] => msg set
@@ -43,7 +40,6 @@
              that is sent to it; it must note such things if/when received*)
   sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Enemy} then {X} else {})"
           (*part of A's internal state*)
-  sees1_Notes "sees1 A (Notes A' X)   = (if A=A' then {X} else {})"
 
 consts  
   sees :: [agent, event list] => msg set