124 ML_file "Tools/SMT/z3_interface.ML" |
124 ML_file "Tools/SMT/z3_interface.ML" |
125 ML_file "Tools/SMT/z3_proof_parser.ML" |
125 ML_file "Tools/SMT/z3_proof_parser.ML" |
126 ML_file "Tools/SMT/z3_proof_tools.ML" |
126 ML_file "Tools/SMT/z3_proof_tools.ML" |
127 ML_file "Tools/SMT/z3_proof_literals.ML" |
127 ML_file "Tools/SMT/z3_proof_literals.ML" |
128 ML_file "Tools/SMT/z3_proof_methods.ML" |
128 ML_file "Tools/SMT/z3_proof_methods.ML" |
|
129 named_theorems z3_simp "simplification rules for Z3 proof reconstruction" |
129 ML_file "Tools/SMT/z3_proof_reconstruction.ML" |
130 ML_file "Tools/SMT/z3_proof_reconstruction.ML" |
130 ML_file "Tools/SMT/z3_model.ML" |
131 ML_file "Tools/SMT/z3_model.ML" |
131 ML_file "Tools/SMT/smt_setup_solvers.ML" |
132 ML_file "Tools/SMT/smt_setup_solvers.ML" |
132 |
133 |
133 setup {* |
134 setup {* |
134 SMT_Config.setup #> |
135 SMT_Config.setup #> |
135 SMT_Normalize.setup #> |
136 SMT_Normalize.setup #> |
136 SMTLIB_Interface.setup #> |
137 SMTLIB_Interface.setup #> |
137 Z3_Interface.setup #> |
138 Z3_Interface.setup #> |
138 Z3_Proof_Reconstruction.setup #> |
|
139 SMT_Setup_Solvers.setup |
139 SMT_Setup_Solvers.setup |
140 *} |
140 *} |
141 |
141 |
142 method_setup smt = {* |
142 method_setup smt = {* |
143 Scan.optional Attrib.thms [] >> |
143 Scan.optional Attrib.thms [] >> |