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.
avoid duplicate fact bindings;
authorwenzelm
Tue, 27 Aug 2002 11:03:02 +0200
changeset 13523 079af5c90d1c
parent 13522 934fffeb6f38
child 13524 604d0f3622d6
avoid duplicate fact bindings;
src/HOL/Auth/Guard/Guard_Shared.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Auth/Guard/Guard_Shared.thy	Tue Aug 27 10:59:21 2002 +0200
+++ b/src/HOL/Auth/Guard/Guard_Shared.thy	Tue Aug 27 11:03:02 2002 +0200
@@ -99,7 +99,7 @@
 lemma guard_ciph [simp]: "shrK A:Ks ==> Ciph A X:guard n Ks"
 by (rule Guard_Nonce, simp)
 
-lemma guard_ciph [simp]: "shrK A:Ks ==> Ciph A X:guardK n Ks"
+lemma guardK_ciph [simp]: "shrK A:Ks ==> Ciph A X:guardK n Ks"
 by (rule Guard_Key, simp)
 
 lemma Guard_init [iff]: "Guard n Ks (initState B)"
isabelle