
diff -r df0f8ad7cc30 -r 5bf2a5c498c2 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Wed Jun 11 08:58:42 2014 +0200
+++ b/src/HOL/Main.thy	Wed Jun 11 11:28:46 2014 +0200
@@ -1,7 +1,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick BNF_GFP
+imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick BNF_GFP SMT
 begin
 
 text {*




