src/HOL/Auth/Smartcard/EventSC.thy

 
 lemma knows_Outpts_secureM: 
       "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*)
 
 

 by (simp add: subset_insertI)
 
 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)"
-by (simp add: subset_insertI)
-
+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")