src/HOL/SMT.thy
changeset 40662 798aad2229c0
parent 40424 7550b2cba1cb
child 40664 e023788a91a1
     1.1 --- a/src/HOL/SMT.thy	Mon Nov 22 14:27:42 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Mon Nov 22 15:45:42 2010 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4    "Tools/Datatype/datatype_selectors.ML"
     1.5    "Tools/SMT/smt_failure.ML"
     1.6    "Tools/SMT/smt_config.ML"
     1.7 +  "Tools/SMT/smt_utils.ML"
     1.8    "Tools/SMT/smt_monomorph.ML"
     1.9    ("Tools/SMT/smt_builtin.ML")
    1.10    ("Tools/SMT/smt_normalize.ML")
    1.11 @@ -19,6 +20,7 @@
    1.12    ("Tools/SMT/z3_proof_parser.ML")
    1.13    ("Tools/SMT/z3_proof_tools.ML")
    1.14    ("Tools/SMT/z3_proof_literals.ML")
    1.15 +  ("Tools/SMT/z3_proof_methods.ML")
    1.16    ("Tools/SMT/z3_proof_reconstruction.ML")
    1.17    ("Tools/SMT/z3_model.ML")
    1.18    ("Tools/SMT/z3_interface.ML")
    1.19 @@ -137,6 +139,7 @@
    1.20  use "Tools/SMT/z3_proof_parser.ML"
    1.21  use "Tools/SMT/z3_proof_tools.ML"
    1.22  use "Tools/SMT/z3_proof_literals.ML"
    1.23 +use "Tools/SMT/z3_proof_methods.ML"
    1.24  use "Tools/SMT/z3_proof_reconstruction.ML"
    1.25  use "Tools/SMT/z3_model.ML"
    1.26  use "Tools/SMT/smt_setup_solvers.ML"