equal
deleted
inserted
replaced
175 else |
175 else |
176 [Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) |
176 [Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) |
177 |
177 |
178 val smt_methodss = |
178 val smt_methodss = |
179 if smt_proofs then |
179 if smt_proofs then |
180 [SMT_Method SMT_Default :: |
180 [SMT_Method SMT_Z3 :: |
181 map (fn strategy => SMT_Method (SMT_Verit strategy)) |
181 map (fn strategy => SMT_Method (SMT_Verit strategy)) |
182 (Verit_Proof.all_veriT_stgies (Context.Proof ctxt))] |
182 (Verit_Proof.all_veriT_stgies (Context.Proof ctxt))] |
183 else |
183 else |
184 [] |
184 [] |
185 in |
185 in |