Replaced setsolver by addsolver
authornipkow
Wed May 29 13:34:17 1996 +0200 (1996-05-29)
changeset 1771ee81183a77a0
parent 1770 608050b43bee
child 1772 ee2be39126d2
Replaced setsolver by addsolver
src/HOL/WF.ML
     1.1 --- a/src/HOL/WF.ML	Wed May 29 12:03:32 1996 +0200
     1.2 +++ b/src/HOL/WF.ML	Wed May 29 13:34:17 1996 +0200
     1.3 @@ -87,11 +87,10 @@
     1.4  
     1.5  (*** NOTE! some simplifications need a different finish_tac!! ***)
     1.6  fun indhyp_tac hyps =
     1.7 -    resolve_tac (TrueI::refl::hyps) ORELSE' 
     1.8      (cut_facts_tac hyps THEN'
     1.9         DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
    1.10                          eresolve_tac [transD, mp, allE]));
    1.11 -val wf_super_ss = HOL_ss setsolver indhyp_tac;
    1.12 +val wf_super_ss = HOL_ss addsolver indhyp_tac;
    1.13  
    1.14  val prems = goalw WF.thy [is_recfun_def,cut_def]
    1.15      "[| wf(r);  trans(r);  is_recfun r H a f;  is_recfun r H b g |] ==> \