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.
Now possibility_tac is an explicit function, in order to delay
authorpaulson
Tue, 22 Jul 1997 11:49:44 +0200
changeset 3544 6ae62d55a620
parent 3543 82f33248d89d
child 3545 4336eb0486bc
Now possibility_tac is an explicit function, in order to delay the evaluation of \!simpset
src/HOL/Auth/Public.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Auth/Public.ML	Tue Jul 22 11:26:02 1997 +0200
+++ b/src/HOL/Auth/Public.ML	Tue Jul 22 11:49:44 1997 +0200
@@ -129,7 +129,7 @@
 qed "Nonce_supply";
 
 (*Tactic for possibility theorems*)
-val possibility_tac =
+fun possibility_tac st = st |>
     REPEAT (*omit used_Says so that Nonces, Keys start from different traces!*)
     (ALLGOALS (simp_tac (!simpset delsimps [used_Says] setSolver safe_solver))
      THEN
isabelle