Slightly generalized the agents' knowledge theorems

--- a/src/HOL/Auth/Event_lemmas.ML	Thu Dec 06 22:38:50 2001 +0100
+++ b/src/HOL/Auth/Event_lemmas.ML	Fri Dec 07 11:10:54 2001 +0100
@@ -88,15 +88,15 @@
 qed "knows_Gets";
 
 
-Goal "knows A evs <= knows A (Says A B X # evs)";
+Goal "knows A evs <= knows A (Says A' B X # evs)";
 by (simp_tac (simpset() addsimps [subset_insertI]) 1);
 qed "knows_subset_knows_Says";
 
-Goal "knows A evs <= knows A (Notes A X # evs)";
+Goal "knows A evs <= knows A (Notes A' X # evs)";
 by (simp_tac (simpset() addsimps [subset_insertI]) 1);
 qed "knows_subset_knows_Notes";
 
-Goal "knows A evs <= knows A (Gets A X # evs)";
+Goal "knows A evs <= knows A (Gets A' X # evs)";
 by (simp_tac (simpset() addsimps [subset_insertI]) 1);
 qed "knows_subset_knows_Gets";
 

--- a/src/HOL/Auth/Shared.thy	Thu Dec 06 22:38:50 2001 +0100
+++ b/src/HOL/Auth/Shared.thy	Fri Dec 07 11:10:54 2001 +0100
@@ -57,4 +57,7 @@
             gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
     "for proving possibility theorems"
 
+lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
+by (induct e, auto simp: knows_Cons)
+
 end