equal
deleted
inserted
replaced
1 (* Title: HOL/TPTP/atp_problem_import.ML |
1 Nitpick_Commands(* Title: HOL/TPTP/atp_problem_import.ML |
2 Author: Jasmin Blanchette, TU Muenchen |
2 Author: Jasmin Blanchette, TU Muenchen |
3 Copyright 2012 |
3 Copyright 2012 |
4 |
4 |
5 Import TPTP problems as Isabelle terms or goals. |
5 Import TPTP problems as Isabelle terms or goals. |
6 *) |
6 *) |
91 ("show_consts", "true"), |
91 ("show_consts", "true"), |
92 ("format", "1"), |
92 ("format", "1"), |
93 ("max_potential", "0"), |
93 ("max_potential", "0"), |
94 ("timeout", string_of_int timeout), |
94 ("timeout", string_of_int timeout), |
95 ("tac_timeout", string_of_int ((timeout + 49) div 50))] |
95 ("tac_timeout", string_of_int ((timeout + 49) div 50))] |
96 |> Nitpick_Isar.default_params thy |
96 |> Nitpick_Commands.default_params thy |
97 val i = 1 |
97 val i = 1 |
98 val n = 1 |
98 val n = 1 |
99 val step = 0 |
99 val step = 0 |
100 val subst = [] |
100 val subst = [] |
101 in |
101 in |
166 ("verbose", "true"), |
166 ("verbose", "true"), |
167 ("debug", if debug then "true" else "false"), |
167 ("debug", if debug then "true" else "false"), |
168 ("overlord", if overlord then "true" else "false"), |
168 ("overlord", if overlord then "true" else "false"), |
169 ("max_potential", "0"), |
169 ("max_potential", "0"), |
170 ("timeout", string_of_int timeout)] |
170 ("timeout", string_of_int timeout)] |
171 |> Nitpick_Isar.default_params thy |
171 |> Nitpick_Commands.default_params thy |
172 val i = 1 |
172 val i = 1 |
173 val n = 1 |
173 val n = 1 |
174 val step = 0 |
174 val step = 0 |
175 val subst = [] |
175 val subst = [] |
176 val (outcome, _) = |
176 val (outcome, _) = |