equal
deleted
inserted
replaced
125 |
125 |
126 method_setup smt = {* |
126 method_setup smt = {* |
127 Scan.optional Attrib.thms [] >> |
127 Scan.optional Attrib.thms [] >> |
128 (fn thms => fn ctxt => |
128 (fn thms => fn ctxt => |
129 METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts)))) |
129 METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts)))) |
130 *} "apply an SMT solver to the current goal (based on SMT-LIB 2)" |
130 *} "apply an SMT solver to the current goal" |
131 |
131 |
132 |
132 |
133 subsection {* Configuration *} |
133 subsection {* Configuration *} |
134 |
134 |
135 text {* |
135 text {* |