# HG changeset patch
# User wenzelm
# Date 1205775422 -3600
# Node ID 28193aedc718f96911857727937aa2ddfdd51f06
# Parent  03def556e26e81686f29a32c989c560e4629462c
renamed K3_imp_Gets variant to K3_imp_Gets_evs;

diff -r 03def556e26e -r 28193aedc718 src/HOL/Auth/KerberosIV_Gets.thy
--- a/src/HOL/Auth/KerberosIV_Gets.thy	Mon Mar 17 18:37:00 2008 +0100
+++ b/src/HOL/Auth/KerberosIV_Gets.thy	Mon Mar 17 18:37:02 2008 +0100
@@ -1404,7 +1404,7 @@
 done
 
 
-lemma K3_imp_Gets:
+lemma K3_imp_Gets_evs:
   "\<lbrakk> Says A Tgs \<lbrace>Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>,
                  Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace> 
       \<in> set evs;  A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
@@ -1429,7 +1429,7 @@
 apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst], assumption)
 apply (drule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd, THEN parts.Fst], assumption)
 apply (drule Tgs_authenticates_A, assumption+, simp)
-apply (force dest!: K3_imp_Gets Gets_imp_knows [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
+apply (force dest!: K3_imp_Gets_evs Gets_imp_knows [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
 done
 
 lemma K4_imp_Gets: