101 these (AList.lookup (op =) infers ident) |> inference_term |
101 these (AList.lookup (op =) infers ident) |> inference_term |
102 fun add_inferences_to_problem_line infers |
102 fun add_inferences_to_problem_line infers |
103 (Formula (ident, Axiom, phi, NONE, NONE)) = |
103 (Formula (ident, Axiom, phi, NONE, NONE)) = |
104 Formula (ident, Lemma, phi, inference infers ident, NONE) |
104 Formula (ident, Lemma, phi, inference infers ident, NONE) |
105 | add_inferences_to_problem_line _ line = line |
105 | add_inferences_to_problem_line _ line = line |
106 val add_inferences_to_problem = |
106 fun add_inferences_to_problem infers = |
107 map o apsnd o map o add_inferences_to_problem_line |
107 map (apsnd (map (add_inferences_to_problem_line infers))) |
108 |
108 |
109 fun ident_of_problem_line (Decl (ident, _, _)) = ident |
109 fun ident_of_problem_line (Decl (ident, _, _)) = ident |
110 | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident |
110 | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident |
111 |
111 |
112 fun run_some_atp ctxt problem = |
112 fun run_some_atp ctxt problem = |