--- 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