src/HOL/SMT/SMT_Base.thy
changeset 36891 e0d295cb8bfd
parent 36884 88cf4896b980
child 36893 48cf03469dc6
--- 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"