| changeset 71794 | ac28714b7478 |
| parent 69706 | 6d6235b828fc |
| child 72584 | 4ea19e5dc67e |
| 71793:e771b8157fc7 | 71794:ac28714b7478 |
|---|---|
83 | try_methss ress (meths :: methss) = |
83 | try_methss ress (meths :: methss) = |
84 let |
84 let |
85 fun mk_step fact_names meths = |
85 fun mk_step fact_names meths = |
86 Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "") |
86 Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "") |
87 in |
87 in |
88 (case preplay_isar_step ctxt chained timeout [] (mk_step fact_names meths) of |
88 (case preplay_isar_step ctxt [] timeout [] (mk_step fact_names meths) of |
89 (res as (meth, Played time)) :: _ => |
89 (res as (meth, Played time)) :: _ => |
90 (* if a fact is needed by an ATP, it will be needed by "metis" *) |
90 (* if a fact is needed by an ATP, it will be needed by "metis" *) |
91 if not minimize orelse is_metis_method meth then |
91 if not minimize orelse is_metis_method meth then |
92 (used_facts, res) |
92 (used_facts, res) |
93 else |
93 else |