# HG changeset patch
# User paulson
# Date 843495578 -7200
# Node ID 1b234f1fd9c74fd42ec3c0c3118b541813406ba2
# Parent  d9af64c26be6c1f95c73b11d0b9ff8ceeadf8277
Removal of the Notes constructor

diff -r d9af64c26be6 -r 1b234f1fd9c7 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Mon Sep 23 18:19:02 1996 +0200
+++ b/src/HOL/Auth/Shared.ML	Mon Sep 23 18:19:38 1996 +0200
@@ -145,11 +145,6 @@
 by (Fast_tac 1);
 qed "sees_Says_subset_insert";
 
-goal thy "sees A (Notes A' X # evs) <= insert X (sees A evs)";
-by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Fast_tac 1);
-qed "sees_Notes_subset_insert";
-
 goal thy "sees A evs <= sees A (Says A' B X # evs)";
 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
 by (Fast_tac 1);
@@ -180,7 +175,6 @@
 
 goal thy "X : sees C evs --> \
 \          (EX A B. Says A B X : set_of_list evs) | \
-\          (EX A. Notes A X : set_of_list evs) | \
 \          (EX A. X = Key (shrK A))";
 by (list.induct_tac "evs" 1);
 by (ALLGOALS Asm_simp_tac);
@@ -245,3 +239,10 @@
 	   ]) i;
 
 
+(** Simplifying   parts (insert X (sees A evs))
+                = parts {X} Un parts (sees A evs) -- since general case loops*)
+
+val parts_insert_sees = 
+    parts_insert |> read_instantiate_sg (sign_of thy) [("H", "sees A evs")]
+                 |> standard;
+
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