src/HOL/SMT/SMT_Base.thy

--- a/src/HOL/SMT/SMT_Base.thy	Wed May 12 23:53:54 2010 +0200
+++ b/src/HOL/SMT/SMT_Base.thy	Wed May 12 23:53:55 2010 +0200
@@ -8,6 +8,7 @@
 imports Real "~~/src/HOL/Word/Word"
 uses
   "~~/src/Tools/cache_io.ML"
+  ("Tools/smt_additional_facts.ML")
   ("Tools/smt_normalize.ML")
   ("Tools/smt_monomorph.ML")
   ("Tools/smt_translate.ML")
@@ -130,6 +131,7 @@
 
 section {* Setup *}
 
+use "Tools/smt_additional_facts.ML"
 use "Tools/smt_normalize.ML"
 use "Tools/smt_monomorph.ML"
 use "Tools/smt_translate.ML"