equal
deleted
inserted
replaced
307 th |> transform_elim_theorem |
307 th |> transform_elim_theorem |
308 |> zero_var_indexes |
308 |> zero_var_indexes |
309 |> new_skolemizer ? forall_intr_vars |
309 |> new_skolemizer ? forall_intr_vars |
310 val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single |
310 val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single |
311 val th = th |> Conv.fconv_rule Object_Logic.atomize |
311 val th = th |> Conv.fconv_rule Object_Logic.atomize |
312 |> abs_extensionalize_thm ctxt |> make_nnf ctxt |
312 |> cong_extensionalize_thm thy |
|
313 |> abs_extensionalize_thm ctxt |
|
314 |> make_nnf ctxt |
313 in |
315 in |
314 if new_skolemizer then |
316 if new_skolemizer then |
315 let |
317 let |
316 fun skolemize choice_ths = |
318 fun skolemize choice_ths = |
317 skolemize_with_choice_theorems ctxt choice_ths |
319 skolemize_with_choice_theorems ctxt choice_ths |