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/HOL/Prolog/prolog.ML
changeset 32282 853ef99c04cc
parent 32260 eb97888fa422
child 32283 3bebc195c124 
--- a/src/HOL/Prolog/prolog.ML	Thu Jul 30 11:23:17 2009 +0200
+++ b/src/HOL/Prolog/prolog.ML	Thu Jul 30 11:23:57 2009 +0200
@@ -67,7 +67,7 @@
         imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
         imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
 
-(*val hyp_resolve_tac = FOCUS (fn {prems, ...} =>
+(*val hyp_resolve_tac = FOCUS_PREMS (fn {prems, ...} =>
                                   resolve_tac (maps atomizeD prems) 1);
   -- is nice, but cannot instantiate unknowns in the assumptions *)
 fun hyp_resolve_tac i st = let
isabelle