Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Auth/Guard/Proto.thy
changeset 81543 fa37ee54644c
parent 76290 64d29ebb7d3d 
--- a/src/HOL/Auth/Guard/Proto.thy	Tue Dec 03 22:46:24 2024 +0100
+++ b/src/HOL/Auth/Guard/Proto.thy	Fri Dec 06 13:33:25 2024 +0100
@@ -464,7 +464,7 @@
 apply (frule Guard_safe, simp)
 apply (frule Crypt_guard_invKey, simp)
 apply (frule ok_Guard, simp, simp, simp, clarsimp)
-apply (frule_tac K="pubK' s b" in Crypt_guard_invKey, simp)
+apply (frule_tac K="pubK' s Proto.b" in Crypt_guard_invKey, simp)
 apply (frule_tac R=ns1 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
 apply (simp add: secret_def, simp add: secret_def, force, force)
 apply (simp add: secret_def keys_def, blast)
@@ -475,7 +475,7 @@
 apply (frule Guard_safe, simp)
 apply (frule Crypt_guard_invKey, simp)
 apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp)
-apply (frule_tac K="pubK' s a" in Crypt_guard_invKey, simp)
+apply (frule_tac K="pubK' s Proto.a" in Crypt_guard_invKey, simp)
 apply (frule_tac R=ns1 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
 apply (simp add: secret_def, simp add: secret_def, force, force)
 apply (simp add: secret_def, rule No_Nonce, simp)
@@ -493,7 +493,7 @@
 apply (frule Guard_safe, simp)
 apply (frule Crypt_guard_invKey, simp)
 apply (frule ok_Guard, simp, simp, simp, clarsimp)
-apply (frule_tac K="pubK' s b" in Crypt_guard_invKey, simp)
+apply (frule_tac K="pubK' s Proto.b" in Crypt_guard_invKey, simp)
 apply (frule_tac R=ns2 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
 apply (simp add: secret_def, simp add: secret_def, force, force)
 apply (simp add: secret_def, rule No_Nonce, simp)
@@ -503,7 +503,7 @@
 apply (frule Guard_safe, simp)
 apply (frule Crypt_guard_invKey, simp)
 apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp)
-apply (frule_tac K="pubK' s a" in Crypt_guard_invKey, simp)
+apply (frule_tac K="pubK' s Proto.a" in Crypt_guard_invKey, simp)
 apply (frule_tac R=ns2 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
 apply (simp add: secret_def, simp add: secret_def, force, force)
 apply (simp add: secret_def keys_def, blast)
isabelle