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/WF.ML
changeset 7570 a9391550eea1
parent 7499 23e090051cb8
child 8265 187cada50e19 
--- a/src/HOL/WF.ML	Tue Sep 21 19:10:39 1999 +0200
+++ b/src/HOL/WF.ML	Tue Sep 21 19:11:07 1999 +0200
@@ -260,7 +260,7 @@
     (cut_facts_tac hyps THEN'
        DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
                         eresolve_tac [transD, mp, allE]));
-val wf_super_ss = HOL_ss addSolver indhyp_tac;
+val wf_super_ss = HOL_ss addSolver (mk_solver "WF" indhyp_tac);
 
 Goalw [is_recfun_def,cut_def]
     "[| wf(r);  trans(r);  is_recfun r H a f;  is_recfun r H b g |] ==> \
isabelle