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.
src/ZF/UNITY/SubstAx.thy
changeset 58963 26bf09b95dda
parent 58871 c399ae4b836f
child 59755 f8d164ab0dc1 
--- a/src/ZF/UNITY/SubstAx.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/ZF/UNITY/SubstAx.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -352,7 +352,7 @@
 (*proves "ensures/leadsTo" properties when the program is specified*)
 fun ensures_tac ctxt sact =
   SELECT_GOAL
-    (EVERY [REPEAT (Always_Int_tac 1),
+    (EVERY [REPEAT (Always_Int_tac ctxt 1),
             etac @{thm Always_LeadsTo_Basis} 1
                 ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
                 REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
isabelle