equal
deleted
inserted
replaced
143 val preferred = |
143 val preferred = |
144 if smt_proofs then |
144 if smt_proofs then |
145 SMT_Method (if name = "z3" then SMT_Z3 else SMT_Verit "default") |
145 SMT_Method (if name = "z3" then SMT_Z3 else SMT_Verit "default") |
146 else |
146 else |
147 Metis_Method (NONE, NONE); |
147 Metis_Method (NONE, NONE); |
148 val methss = bunches_of_proof_methods ctxt try0 smt_proofs false liftingN; |
148 val methss = |
|
149 if try0 then |
|
150 bunches_of_proof_methods ctxt smt_proofs false liftingN |
|
151 else |
|
152 [[preferred]] |
149 in |
153 in |
150 ((preferred, methss), |
154 ((preferred, methss), |
151 fn preplay => |
155 fn preplay => |
152 let |
156 let |
153 val _ = if verbose then writeln "Generating proof text..." else () |
157 val _ = if verbose then writeln "Generating proof text..." else () |