equal
deleted
inserted
replaced
140 exists (fn prefix => String.isPrefix prefix ident) |
140 exists (fn prefix => String.isPrefix prefix ident) |
141 likely_tautology_prefixes andalso |
141 likely_tautology_prefixes andalso |
142 is_none (run_some_atp ctxt format |
142 is_none (run_some_atp ctxt format |
143 [(factsN, [Formula (ident, Conjecture, phi, NONE, [])])]) |
143 [(factsN, [Formula (ident, Conjecture, phi, NONE, [])])]) |
144 | is_problem_line_tautology _ _ _ = false |
144 | is_problem_line_tautology _ _ _ = false |
145 |
|
146 structure String_Graph = Graph(type key = string val ord = string_ord); |
|
147 |
145 |
148 fun order_facts ord = sort (ord o pairself ident_of_problem_line) |
146 fun order_facts ord = sort (ord o pairself ident_of_problem_line) |
149 fun order_problem_facts _ [] = [] |
147 fun order_problem_facts _ [] = [] |
150 | order_problem_facts ord ((heading, lines) :: problem) = |
148 | order_problem_facts ord ((heading, lines) :: problem) = |
151 if heading = factsN then (heading, order_facts ord lines) :: problem |
149 if heading = factsN then (heading, order_facts ord lines) :: problem |