102 |> Skip_Proof.make_thm thy |
102 |> Skip_Proof.make_thm thy |
103 end |
103 end |
104 |
104 |
105 fun tac_of_method method type_enc lam_trans ctxt facts = |
105 fun tac_of_method method type_enc lam_trans ctxt facts = |
106 (case method of |
106 (case method of |
107 MetisM => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts |
107 Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts |
108 | MesonM => Meson.meson_tac ctxt facts |
108 | Meson_Method => Meson.meson_tac ctxt facts |
109 | _ => |
109 | _ => |
110 Method.insert_tac facts THEN' |
110 Method.insert_tac facts THEN' |
111 (case method of |
111 (case method of |
112 SimpM => Simplifier.asm_full_simp_tac ctxt |
112 Simp_Method => Simplifier.asm_full_simp_tac ctxt |
113 | AutoM => K (Clasimp.auto_tac ctxt) |
113 | Auto_Method => K (Clasimp.auto_tac ctxt) |
114 | FastforceM => Clasimp.fast_force_tac ctxt |
114 | Fastforce_Method => Clasimp.fast_force_tac ctxt |
115 | ForceM => Clasimp.force_tac ctxt |
115 | Force_Method => Clasimp.force_tac ctxt |
116 | ArithM => Arith_Data.arith_tac ctxt |
116 | Arith_Method => Arith_Data.arith_tac ctxt |
117 | BlastM => blast_tac ctxt |
117 | Blast_Method => blast_tac ctxt |
118 | _ => raise Fail "Sledgehammer_Preplay: tac_of_method")) |
118 | _ => raise Fail "Sledgehammer_Preplay: tac_of_method")) |
119 |
119 |
120 (* main function for preplaying Isar steps; may throw exceptions *) |
120 (* main function for preplaying Isar steps; may throw exceptions *) |
121 fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time |
121 fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time |
122 | preplay_raw debug type_enc lam_trans ctxt timeout |
122 | preplay_raw debug type_enc lam_trans ctxt timeout |