src/HOL/SMT.thy
changeset 41174 10eb369f8c01
parent 41127 2ea84c8535c6
child 41280 a7de9d36f4f2
     1.1 --- a/src/HOL/SMT.thy	Wed Dec 15 16:32:45 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Wed Dec 15 18:18:56 2010 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4    "Tools/SMT/smt_utils.ML"
     1.5    "Tools/SMT/smt_failure.ML"
     1.6    "Tools/SMT/smt_config.ML"
     1.7 -  "Tools/SMT/smt_monomorph.ML"
     1.8 +  ("Tools/SMT/smt_monomorph.ML")
     1.9    ("Tools/SMT/smt_builtin.ML")
    1.10    ("Tools/SMT/smt_normalize.ML")
    1.11    ("Tools/SMT/smt_translate.ML")
    1.12 @@ -149,6 +149,7 @@
    1.13  
    1.14  subsection {* Setup *}
    1.15  
    1.16 +use "Tools/SMT/smt_monomorph.ML"
    1.17  use "Tools/SMT/smt_builtin.ML"
    1.18  use "Tools/SMT/smt_normalize.ML"
    1.19  use "Tools/SMT/smt_translate.ML"