| changeset 2637 | e9b203f854ae |
| parent 2482 | 87383dd9f4b5 |
| child 3016 | 15763781afb0 |
--- a/src/ZF/WF.ML Sat Feb 15 17:48:19 1997 +0100 +++ b/src/ZF/WF.ML Sat Feb 15 17:52:31 1997 +0100 @@ -225,7 +225,7 @@ eresolve_tac [underD, transD, spec RS mp])); (*** NOTE! some simplifications need a different solver!! ***) -val wf_super_ss = !simpset setsolver indhyp_tac; +val wf_super_ss = !simpset setSolver indhyp_tac; val prems = goalw WF.thy [is_recfun_def] "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] ==> \