equal
deleted
inserted
replaced
172 val xweightsN = "_weights" |
172 val xweightsN = "_weights" |
173 val xprecN = "_prec" |
173 val xprecN = "_prec" |
174 val xsimpN = "_simp" (* SPASS-specific *) |
174 val xsimpN = "_simp" (* SPASS-specific *) |
175 |
175 |
176 (* Possible values for "atp_term_order": |
176 (* Possible values for "atp_term_order": |
177 "smart", "(kbo(_weights)?|lpo)(_prec|_simp)?" *) |
177 "smart", "(kbo|lpo)(_weights)?(_prec|_simp)?" *) |
178 val term_order = |
178 val term_order = |
179 Attrib.setup_config_string @{binding atp_term_order} (K smartN) |
179 Attrib.setup_config_string @{binding atp_term_order} (K smartN) |
180 |
180 |
181 fun effective_term_order ctxt atp = |
181 fun effective_term_order ctxt atp = |
182 let val ord = Config.get ctxt term_order in |
182 let val ord = Config.get ctxt term_order in |