src/ZF/WF.ML
 changeset 443 10884e64c241 parent 437 435875e4b21d child 485 5e00a676a211
equal inserted replaced
442:13ac1fd0a14d 443:10884e64c241
`   215 by (assume_tac 1);`
`   215 by (assume_tac 1);`
`   216 val is_recfun_type = result();`
`   216 val is_recfun_type = result();`
`   217 `
`   217 `
`   218 val [isrec,rel] = goalw WF.thy [is_recfun_def]`
`   218 val [isrec,rel] = goalw WF.thy [is_recfun_def]`
`   219     "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))";`
`   219     "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))";`
`   220 by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (isrec RS ssubst) 1);`
`   220 by (res_inst_tac [("P", "%x.?t(x) = (?u::i)")] (isrec RS ssubst) 1);`
`   221 by (rtac (rel RS underI RS beta) 1);`
`   221 by (rtac (rel RS underI RS beta) 1);`
`   222 val apply_recfun = result();`
`   222 val apply_recfun = result();`
`   223 `
`   223 `
`   224 (*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE`
`   224 (*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE`
`   225   spec RS mp  instantiates induction hypotheses*)`
`   225   spec RS mp  instantiates induction hypotheses*)`