--- a/src/HOL/SMT.thy Wed Aug 22 22:55:41 2012 +0200
+++ b/src/HOL/SMT.thy Wed Aug 22 23:22:57 2012 +0200
@@ -7,26 +7,11 @@
theory SMT
imports Record
keywords "smt_status" :: diag
-uses
- "Tools/SMT/smt_utils.ML"
- "Tools/SMT/smt_failure.ML"
- "Tools/SMT/smt_config.ML"
- ("Tools/SMT/smt_builtin.ML")
- ("Tools/SMT/smt_datatypes.ML")
- ("Tools/SMT/smt_normalize.ML")
- ("Tools/SMT/smt_translate.ML")
- ("Tools/SMT/smt_solver.ML")
- ("Tools/SMT/smtlib_interface.ML")
- ("Tools/SMT/z3_interface.ML")
- ("Tools/SMT/z3_proof_parser.ML")
- ("Tools/SMT/z3_proof_tools.ML")
- ("Tools/SMT/z3_proof_literals.ML")
- ("Tools/SMT/z3_proof_methods.ML")
- ("Tools/SMT/z3_proof_reconstruction.ML")
- ("Tools/SMT/z3_model.ML")
- ("Tools/SMT/smt_setup_solvers.ML")
begin
+ML_file "Tools/SMT/smt_utils.ML"
+ML_file "Tools/SMT/smt_failure.ML"
+ML_file "Tools/SMT/smt_config.ML"
subsection {* Triggers for quantifier instantiation *}
@@ -135,20 +120,20 @@
subsection {* Setup *}
-use "Tools/SMT/smt_builtin.ML"
-use "Tools/SMT/smt_datatypes.ML"
-use "Tools/SMT/smt_normalize.ML"
-use "Tools/SMT/smt_translate.ML"
-use "Tools/SMT/smt_solver.ML"
-use "Tools/SMT/smtlib_interface.ML"
-use "Tools/SMT/z3_interface.ML"
-use "Tools/SMT/z3_proof_parser.ML"
-use "Tools/SMT/z3_proof_tools.ML"
-use "Tools/SMT/z3_proof_literals.ML"
-use "Tools/SMT/z3_proof_methods.ML"
-use "Tools/SMT/z3_proof_reconstruction.ML"
-use "Tools/SMT/z3_model.ML"
-use "Tools/SMT/smt_setup_solvers.ML"
+ML_file "Tools/SMT/smt_builtin.ML"
+ML_file "Tools/SMT/smt_datatypes.ML"
+ML_file "Tools/SMT/smt_normalize.ML"
+ML_file "Tools/SMT/smt_translate.ML"
+ML_file "Tools/SMT/smt_solver.ML"
+ML_file "Tools/SMT/smtlib_interface.ML"
+ML_file "Tools/SMT/z3_interface.ML"
+ML_file "Tools/SMT/z3_proof_parser.ML"
+ML_file "Tools/SMT/z3_proof_tools.ML"
+ML_file "Tools/SMT/z3_proof_literals.ML"
+ML_file "Tools/SMT/z3_proof_methods.ML"
+ML_file "Tools/SMT/z3_proof_reconstruction.ML"
+ML_file "Tools/SMT/z3_model.ML"
+ML_file "Tools/SMT/smt_setup_solvers.ML"
setup {*
SMT_Config.setup #>