equal
deleted
inserted
replaced
124 |>> map string_for_label |
124 |>> map string_for_label |
125 |> op @ |
125 |> op @ |
126 |> maps (thms_of_name ctxt) |
126 |> maps (thms_of_name ctxt) |
127 |
127 |
128 (* TODO: add "Obtain" case *) |
128 (* TODO: add "Obtain" case *) |
129 exception ZeroTime |
129 exception ZEROTIME |
130 fun try_metis timeout (succedent, step) = |
130 fun try_metis timeout (succedent, step) = |
131 (if not preplay then K (SOME Time.zeroTime) else |
131 (if not preplay then K (SOME Time.zeroTime) else |
132 let |
132 let |
133 val (t, byline, obtain) = |
133 val (t, byline, obtain) = |
134 (case step of |
134 (case step of |
156 |> (fn t => HOLogic.mk_all ("thesis", HOLogic.boolT, t)) |
156 |> (fn t => HOLogic.mk_all ("thesis", HOLogic.boolT, t)) |
157 |> HOLogic.mk_Trueprop |
157 |> HOLogic.mk_Trueprop |
158 in |
158 in |
159 (prop, byline, true) |
159 (prop, byline, true) |
160 end |
160 end |
161 | _ => raise ZeroTime) |
161 | _ => raise ZEROTIME) |
162 val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |
162 val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |
163 val facts = |
163 val facts = |
164 (case byline of |
164 (case byline of |
165 By_Metis fact_names => resolve_fact_names fact_names |
165 By_Metis fact_names => resolve_fact_names fact_names |
166 | Case_Split (cases, fact_names) => |
166 | Case_Split (cases, fact_names) => |
181 fun tac {context = ctxt, prems = _} = |
181 fun tac {context = ctxt, prems = _} = |
182 Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 |
182 Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 |
183 in |
183 in |
184 take_time timeout (fn () => goal tac) |
184 take_time timeout (fn () => goal tac) |
185 end) |
185 end) |
186 handle ZeroTime => K (SOME Time.zeroTime) |
186 handle ZEROTIME => K (SOME Time.zeroTime) |
187 |
187 |
188 val try_metis_quietly = the_default NONE oo try oo try_metis |
188 val try_metis_quietly = the_default NONE oo try oo try_metis |
189 |
189 |
190 (* cache metis preplay times in lazy time vector *) |
190 (* cache metis preplay times in lazy time vector *) |
191 val metis_time = |
191 val metis_time = |