# HG changeset patch
# User paulson
# Date 1007719854 -3600
# Node ID 74977582a585c8b7303f2f6bb744ba9cd670c8c1
# Parent  61e1681b0b5d0eafcde31e4d8ce77030d80e966e
Slightly generalized the agents' knowledge theorems

diff -r 61e1681b0b5d -r 74977582a585 src/HOL/Auth/Event_lemmas.ML
--- 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";
 
diff -r 61e1681b0b5d -r 74977582a585 src/HOL/Auth/Shared.thy
--- 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