equal
deleted
inserted
replaced
137 val formula_map : |
137 val formula_map : |
138 ('c -> 'e) -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'e, 'd) atp_formula |
138 ('c -> 'e) -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'e, 'd) atp_formula |
139 val strip_atype : 'a atp_type -> 'a list * ('a atp_type list * 'a atp_type) |
139 val strip_atype : 'a atp_type -> 'a list * ('a atp_type list * 'a atp_type) |
140 val is_format_higher_order : atp_format -> bool |
140 val is_format_higher_order : atp_format -> bool |
141 val tptp_string_of_format : atp_format -> string |
141 val tptp_string_of_format : atp_format -> string |
|
142 val tptp_string_of_role : atp_formula_role -> string |
142 val tptp_string_of_line : atp_format -> string atp_problem_line -> string |
143 val tptp_string_of_line : atp_format -> string atp_problem_line -> string |
143 val lines_of_atp_problem : |
144 val lines_of_atp_problem : |
144 atp_format -> term_order -> (unit -> (string * int) list) |
145 atp_format -> term_order -> (unit -> (string * int) list) |
145 -> string atp_problem -> string list |
146 -> string atp_problem -> string list |
146 val ensure_cnf_problem : |
147 val ensure_cnf_problem : |