equal
deleted
inserted
replaced
153 val th_cls_pairs = |
153 val th_cls_pairs = |
154 map2 (fn j => fn th => |
154 map2 (fn j => fn th => |
155 (Thm.get_name_hint th, |
155 (Thm.get_name_hint th, |
156 th |
156 th |
157 |> Drule.eta_contraction_rule |
157 |> Drule.eta_contraction_rule |
158 |> Meson_Clausify.cnf_axiom {if_simps = true} ctxt new_skolem (lam_trans = combsN) j |
158 |> Meson_Clausify.cnf_axiom Meson.simp_options_all_true ctxt new_skolem |
|
159 (lam_trans = combsN) j |
159 ||> map do_lams)) |
160 ||> map do_lams)) |
160 (0 upto length ths0 - 1) ths0 |
161 (0 upto length ths0 - 1) ths0 |
161 val ths = maps (snd o snd) th_cls_pairs |
162 val ths = maps (snd o snd) th_cls_pairs |
162 val dischargers = map (fst o snd) th_cls_pairs |
163 val dischargers = map (fst o snd) th_cls_pairs |
163 val cls = cls |> map (Drule.eta_contraction_rule #> do_lams) |
164 val cls = cls |> map (Drule.eta_contraction_rule #> do_lams) |