src/HOL/SMT.thy
changeset 43928 24d6e759753f
parent 43927 3a87cb597832
child 43929 61d432e51aff
     1.1 --- a/src/HOL/SMT.thy	Wed Jul 20 09:23:09 2011 +0200
     1.2 +++ b/src/HOL/SMT.thy	Wed Jul 20 09:23:12 2011 +0200
     1.3 @@ -13,6 +13,7 @@
     1.4    ("Tools/SMT/smt_builtin.ML")
     1.5    ("Tools/SMT/smt_datatypes.ML")
     1.6    ("Tools/SMT/smt_normalize.ML")
     1.7 +  ("Tools/lambda_lifting.ML")
     1.8    ("Tools/SMT/smt_translate.ML")
     1.9    ("Tools/SMT/smt_solver.ML")
    1.10    ("Tools/SMT/smtlib_interface.ML")
    1.11 @@ -137,6 +138,7 @@
    1.12  use "Tools/SMT/smt_builtin.ML"
    1.13  use "Tools/SMT/smt_datatypes.ML"
    1.14  use "Tools/SMT/smt_normalize.ML"
    1.15 +use "Tools/lambda_lifting.ML"
    1.16  use "Tools/SMT/smt_translate.ML"
    1.17  use "Tools/SMT/smt_solver.ML"
    1.18  use "Tools/SMT/smtlib_interface.ML"