src/HOL/SMT.thy
changeset 41328 6792a5c92a58
parent 41281 679118e35378
child 41426 09615ed31f04
     1.1 --- a/src/HOL/SMT.thy	Mon Dec 20 21:04:45 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Mon Dec 20 22:02:57 2010 +0100
     1.3 @@ -17,13 +17,13 @@
     1.4    ("Tools/SMT/smt_translate.ML")
     1.5    ("Tools/SMT/smt_solver.ML")
     1.6    ("Tools/SMT/smtlib_interface.ML")
     1.7 +  ("Tools/SMT/z3_interface.ML")
     1.8    ("Tools/SMT/z3_proof_parser.ML")
     1.9    ("Tools/SMT/z3_proof_tools.ML")
    1.10    ("Tools/SMT/z3_proof_literals.ML")
    1.11    ("Tools/SMT/z3_proof_methods.ML")
    1.12    ("Tools/SMT/z3_proof_reconstruction.ML")
    1.13    ("Tools/SMT/z3_model.ML")
    1.14 -  ("Tools/SMT/z3_interface.ML")
    1.15    ("Tools/SMT/smt_setup_solvers.ML")
    1.16  begin
    1.17