src/HOL/SMT.thy
changeset 43927 3a87cb597832
parent 43230 dabf6e311213
child 43928 24d6e759753f
     1.1 --- a/src/HOL/SMT.thy	Wed Jul 20 08:46:17 2011 +0200
     1.2 +++ b/src/HOL/SMT.thy	Wed Jul 20 09:23:09 2011 +0200
     1.3 @@ -10,7 +10,6 @@
     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_builtin.ML")
     1.9    ("Tools/SMT/smt_datatypes.ML")
    1.10    ("Tools/SMT/smt_normalize.ML")
    1.11 @@ -135,7 +134,6 @@
    1.12  
    1.13  subsection {* Setup *}
    1.14  
    1.15 -use "Tools/SMT/smt_monomorph.ML"
    1.16  use "Tools/SMT/smt_builtin.ML"
    1.17  use "Tools/SMT/smt_datatypes.ML"
    1.18  use "Tools/SMT/smt_normalize.ML"