equal
deleted
inserted
replaced
129 val tfree_classes_of_terms : term list -> string list |
129 val tfree_classes_of_terms : term list -> string list |
130 val tvar_classes_of_terms : term list -> string list |
130 val tvar_classes_of_terms : term list -> string list |
131 val type_constrs_of_terms : theory -> term list -> string list |
131 val type_constrs_of_terms : theory -> term list -> string list |
132 val prepare_atp_problem : |
132 val prepare_atp_problem : |
133 Proof.context -> format -> formula_kind -> formula_kind -> type_sys |
133 Proof.context -> format -> formula_kind -> formula_kind -> type_sys |
134 -> bool option -> bool -> bool -> term list -> term |
134 -> bool -> bool -> term list -> term -> ((string * locality) * term) list |
135 -> ((string * locality) * term) list |
|
136 -> string problem * string Symtab.table * int * int |
135 -> string problem * string Symtab.table * int * int |
137 * (string * locality) list vector * int list * int Symtab.table |
136 * (string * locality) list vector * int list * int Symtab.table |
138 val atp_problem_weights : string problem -> (string * real) list |
137 val atp_problem_weights : string problem -> (string * real) list |
139 end; |
138 end; |
140 |
139 |
1831 val aritiesN = "Arities" |
1830 val aritiesN = "Arities" |
1832 val helpersN = "Helper facts" |
1831 val helpersN = "Helper facts" |
1833 val conjsN = "Conjectures" |
1832 val conjsN = "Conjectures" |
1834 val free_typesN = "Type variables" |
1833 val free_typesN = "Type variables" |
1835 |
1834 |
|
1835 val explicit_apply = NONE (* for experimental purposes *) |
|
1836 |
1836 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys |
1837 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys |
1837 explicit_apply readable_names preproc hyp_ts concl_t |
1838 readable_names preproc hyp_ts concl_t facts = |
1838 facts = |
|
1839 let |
1839 let |
1840 val (format, type_sys) = choose_format [format] type_sys |
1840 val (format, type_sys) = choose_format [format] type_sys |
1841 val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = |
1841 val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = |
1842 translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t |
1842 translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t |
1843 facts |
1843 facts |