Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
renamed K3_imp_Gets variant to K3_imp_Gets_evs;
authorwenzelm
Mon, 17 Mar 2008 18:37:02 +0100
changeset 26301 28193aedc718
parent 26300 03def556e26e
child 26302 68b073052e8c
renamed K3_imp_Gets variant to K3_imp_Gets_evs;
src/HOL/Auth/KerberosIV_Gets.thy file | annotate | diff | comparison | revisions 
--- 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:
isabelle