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.
fixed possibility_tac;
authorwenzelm
Fri, 20 Mar 2009 17:04:44 +0100
changeset 30608 d9805c5b5d2e
parent 30607 c3d1590debd8
child 30609 983e8b6e4e69
fixed possibility_tac;
doc-src/TutorialI/Protocol/Public.thy file | annotate | diff | comparison | revisions 
--- a/doc-src/TutorialI/Protocol/Public.thy	Fri Mar 20 15:24:18 2009 +0100
+++ b/doc-src/TutorialI/Protocol/Public.thy	Fri Mar 20 17:04:44 2009 +0100
@@ -152,7 +152,7 @@
 
 (*Tactic for possibility theorems*)
 ML {*
-fun possibility ctxt =
+fun possibility_tac ctxt =
     REPEAT (*omit used_Says so that Nonces start from different traces!*)
     (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says]))
      THEN
isabelle