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 and basic_possibility_tac are explicit functions, in order
authorpaulson
Tue, 22 Jul 1997 11:23:03 +0200
changeset 3542 db5e9aceea49
parent 3541 2f5ac0f047a6
child 3543 82f33248d89d
Now possibility_tac and basic_possibility_tac are explicit functions, in order to delay the evaluation of \!simpset
src/HOL/Auth/Shared.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Auth/Shared.ML	Tue Jul 22 11:21:17 1997 +0200
+++ b/src/HOL/Auth/Shared.ML	Tue Jul 22 11:23:03 1997 +0200
@@ -197,16 +197,16 @@
 
 (*** Tactics for possibility theorems ***)
 
-val possibility_tac =
-    REPEAT (*omit used_Says so that Nonces, Keys start from different traces!*)
+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
      REPEAT_FIRST (eq_assume_tac ORELSE' 
-                   resolve_tac [refl, conjI, Nonce_supply, Key_supply]));
+                   resolve_tac [refl, conjI, Nonce_supply, Key_supply])));
 
 (*For harder protocols (such as Recur) where we have to set up some
   nonces and keys initially*)
-val basic_possibility_tac =
+fun basic_possibility_tac st = st |>
     REPEAT 
     (ALLGOALS (asm_simp_tac (!simpset setSolver safe_solver))
      THEN
isabelle