equal
deleted
inserted
replaced
138 val dischargers = map (fst o snd) th_cls_pairs |
138 val dischargers = map (fst o snd) th_cls_pairs |
139 val cls = cls |> map (Drule.eta_contraction_rule #> do_lams) |
139 val cls = cls |> map (Drule.eta_contraction_rule #> do_lams) |
140 val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") |
140 val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") |
141 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls |
141 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls |
142 val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) |
142 val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) |
143 val type_enc = type_enc_from_string Sound type_enc |
143 val type_enc = type_enc_from_string Strict type_enc |
144 val (sym_tab, axioms, concealed) = |
144 val (sym_tab, axioms, concealed) = |
145 prepare_metis_problem ctxt type_enc lam_trans cls ths |
145 prepare_metis_problem ctxt type_enc lam_trans cls ths |
146 fun get_isa_thm mth Isa_Reflexive_or_Trivial = |
146 fun get_isa_thm mth Isa_Reflexive_or_Trivial = |
147 reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth |
147 reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth |
148 | get_isa_thm mth Isa_Lambda_Lifted = |
148 | get_isa_thm mth Isa_Lambda_Lifted = |