# HG changeset patch
# User wenzelm
# Date 1205775423 -3600
# Node ID 68b073052e8cf320f586455004bc83efb4484553
# Parent  28193aedc718f96911857727937aa2ddfdd51f06
proper naming of knows_Outpts_insecureM, knows_subset_knows_A_Gets;

diff -r 28193aedc718 -r 68b073052e8c src/HOL/Auth/Smartcard/EventSC.thy
--- 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")