src/HOL/SMT.thy
changeset 43929 61d432e51aff
parent 43928 24d6e759753f
child 44087 8e491cb8841c
     1.1 --- a/src/HOL/SMT.thy	Wed Jul 20 09:23:12 2011 +0200
     1.2 +++ b/src/HOL/SMT.thy	Wed Jul 20 12:23:20 2011 +0200
     1.3 @@ -7,13 +7,13 @@
     1.4  theory SMT
     1.5  imports Record
     1.6  uses
     1.7 +  "Tools/lambda_lifting.ML"
     1.8    "Tools/SMT/smt_utils.ML"
     1.9    "Tools/SMT/smt_failure.ML"
    1.10    "Tools/SMT/smt_config.ML"
    1.11    ("Tools/SMT/smt_builtin.ML")
    1.12    ("Tools/SMT/smt_datatypes.ML")
    1.13    ("Tools/SMT/smt_normalize.ML")
    1.14 -  ("Tools/lambda_lifting.ML")
    1.15    ("Tools/SMT/smt_translate.ML")
    1.16    ("Tools/SMT/smt_solver.ML")
    1.17    ("Tools/SMT/smtlib_interface.ML")
    1.18 @@ -138,7 +138,6 @@
    1.19  use "Tools/SMT/smt_builtin.ML"
    1.20  use "Tools/SMT/smt_datatypes.ML"
    1.21  use "Tools/SMT/smt_normalize.ML"
    1.22 -use "Tools/lambda_lifting.ML"
    1.23  use "Tools/SMT/smt_translate.ML"
    1.24  use "Tools/SMT/smt_solver.ML"
    1.25  use "Tools/SMT/smtlib_interface.ML"