src/HOL/SMT.thy
changeset 40277 4e3a3461c1a6
parent 40274 6486c610a549
child 40424 7550b2cba1cb
     1.1 --- a/src/HOL/SMT.thy	Fri Oct 29 18:17:06 2010 +0200
     1.2 +++ b/src/HOL/SMT.thy	Fri Oct 29 18:17:08 2010 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  uses
     1.5    "Tools/Datatype/datatype_selectors.ML"
     1.6    ("Tools/SMT/smt_monomorph.ML")
     1.7 +  ("Tools/SMT/smt_builtin.ML")
     1.8    ("Tools/SMT/smt_normalize.ML")
     1.9    ("Tools/SMT/smt_translate.ML")
    1.10    ("Tools/SMT/smt_solver.ML")
    1.11 @@ -126,6 +127,7 @@
    1.12  subsection {* Setup *}
    1.13  
    1.14  use "Tools/SMT/smt_monomorph.ML"
    1.15 +use "Tools/SMT/smt_builtin.ML"
    1.16  use "Tools/SMT/smt_normalize.ML"
    1.17  use "Tools/SMT/smt_translate.ML"
    1.18  use "Tools/SMT/smt_solver.ML"