equal
deleted
inserted
replaced
514 |
514 |
515 val helper_lines = |
515 val helper_lines = |
516 if helper_lemmas_needed then |
516 if helper_lemmas_needed then |
517 [(helpersN, |
517 [(helpersN, |
518 @{thms waldmeister_fol} |
518 @{thms waldmeister_fol} |
519 |> map (fn th => (("", (Global, General)), preproc (prop_of th))) |
519 |> map (fn th => (("", (Global, General)), preproc (Thm.prop_of th))) |
520 |> map (fn ((s, _) ,t) => mk_formula helper_prefix s Axiom (eq_trm_to_atp thy t)))] |
520 |> map (fn ((s, _) ,t) => mk_formula helper_prefix s Axiom (eq_trm_to_atp thy t)))] |
521 else |
521 else |
522 [] |
522 [] |
523 |
523 |
524 val problem = (factsN, axiom_lines) :: helper_lines @ [(conjN, [conj_line])] |
524 val problem = (factsN, axiom_lines) :: helper_lines @ [(conjN, [conj_line])] |