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.
doc-src/TutorialI/Protocol/Event.thy
changeset 46471 2289a3869c88
parent 42637 381fdcab0f36 
--- a/doc-src/TutorialI/Protocol/Event.thy	Tue Feb 14 20:57:05 2012 +0100
+++ b/doc-src/TutorialI/Protocol/Event.thy	Tue Feb 14 21:19:39 2012 +0100
@@ -139,8 +139,8 @@
 text{*Elimination rules: derive contradictions from old Says events containing
   items known to be fresh*}
 lemmas knows_Spy_partsEs =
-     Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
-     parts.Body [THEN revcut_rl, standard]
+     Says_imp_knows_Spy [THEN parts.Inj, elim_format] 
+     parts.Body [elim_format]
 
 lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
isabelle