equal
deleted
inserted
replaced
140 \<close> |
140 \<close> |
141 |
141 |
142 method_setup old_smt = \<open> |
142 method_setup old_smt = \<open> |
143 Scan.optional Attrib.thms [] >> |
143 Scan.optional Attrib.thms [] >> |
144 (fn thms => fn ctxt => |
144 (fn thms => fn ctxt => |
145 METHOD (fn facts => HEADGOAL (Old_SMT_Solver.smt_tac ctxt (thms @ facts)))) |
145 (legacy_feature "Proof method \"old_smt\" will be discontinued soon -- use \"smt\" instead"; |
|
146 METHOD (fn facts => HEADGOAL (Old_SMT_Solver.smt_tac ctxt (thms @ facts))))) |
146 \<close> "apply an SMT solver to the current goal" |
147 \<close> "apply an SMT solver to the current goal" |
147 |
148 |
148 |
149 |
149 subsection \<open>Configuration\<close> |
150 subsection \<open>Configuration\<close> |
150 |
151 |