equal
deleted
inserted
replaced
569 val def0 = (U.rev_itlist (fn x => fn th => R.rbeta(combination th x)) |
569 val def0 = (U.rev_itlist (fn x => fn th => R.rbeta(combination th x)) |
570 SVrefls def) |
570 SVrefls def) |
571 RS meta_eq_to_obj_eq |
571 RS meta_eq_to_obj_eq |
572 val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0 |
572 val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0 |
573 val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop) |
573 val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop) |
574 val bar = R.MP (R.ISPECL[tych R'abs, tych R1] Thms.SELECT_AX) |
574 val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon |
575 body_th |
575 theory Hilbert_Choice*) |
|
576 thm "Hilbert_Choice.tfl_some" |
|
577 handle ERROR => error |
|
578 "defer_recdef requires theory Main or at least Hilbert_Choice as parent" |
|
579 val bar = R.MP (R.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th |
576 in {theory = theory, R=R1, SV=SV, |
580 in {theory = theory, R=R1, SV=SV, |
577 rules = U.rev_itlist (U.C R.MP) (R.CONJUNCTS bar) def', |
581 rules = U.rev_itlist (U.C R.MP) (R.CONJUNCTS bar) def', |
578 full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)), |
582 full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)), |
579 patterns = pats} |
583 patterns = pats} |
580 end; |
584 end; |