--- a/src/HOL/Auth/Smartcard/EventSC.thy Mon Mar 17 18:37:02 2008 +0100
+++ b/src/HOL/Auth/Smartcard/EventSC.thy Mon Mar 17 18:37:03 2008 +0100
@@ -267,7 +267,7 @@
"secureM \<longrightarrow> knows A (Outpts C A X # evs) = insert X (knows A evs)"
by simp
-lemma knows_Outpts_secureM:
+lemma knows_Outpts_insecureM:
"insecureM \<longrightarrow> knows Spy (Outpts C A X # evs) = insert X (knows Spy evs)"
by simp
(*somewhat equivalent to knows_Spy_Outpts_insecureM*)
@@ -293,11 +293,10 @@
lemma knows_subset_knows_Outpts: "knows A evs \<subseteq> knows A (Outpts C A' X # evs)"
by (simp add: subset_insertI)
-lemma knows_subset_knows_Gets: "knows A evs \<subseteq> knows A (A_Gets A' X # evs)"
+lemma knows_subset_knows_A_Gets: "knows A evs \<subseteq> knows A (A_Gets A' X # evs)"
by (simp add: subset_insertI)
-
text{*Agents know what they say*}
lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs \<longrightarrow> X \<in> knows A evs"
apply (induct_tac "evs")