TFL/tfl.ML
changeset 11455 e07927b980ec
parent 10769 70b9b0cfe05f
child 11632 6fc8de600f58
equal deleted inserted replaced
11454:7514e5e21cb8 11455:e07927b980ec
   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;