diff -r c0056c2c1d17 -r 42865636d006 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Sep 18 14:40:24 2009 +0200
+++ b/src/HOL/IsaMakefile	Fri Sep 18 18:13:19 2009 +0200
@@ -40,6 +40,7 @@
   HOL-Prolog \
   HOL-SET-Protocol \
   HOL-SizeChange \
+  HOL-SMT \
   HOL-Statespace \
   HOL-Subst \
       TLA-Buffer \
@@ -1134,6 +1135,19 @@
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
 
 
+## HOL-SMT
+
+HOL-SMT: HOL-Word $(LOG)/HOL-SMT.gz
+
+$(LOG)/HOL-SMT.gz: $(OUT)/HOL-Word SMT/SMT_Definitions.thy SMT/SMT.thy \
+  SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML \
+  SMT/Tools/smt_translate.ML SMT/Tools/smt_builtin.ML \
+  SMT/Tools/smtlib_interface.ML SMT/Tools/smt_solver.ML \
+  SMT/Tools/cvc3_solver.ML SMT/Tools/yices_solver.ML \
+  SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML SMT/Tools/z3_model.ML
+	@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
+
+
 ## clean
 
 clean:
@@ -1156,4 +1170,4 @@
 		$(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz	\
 		$(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA		\
 		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz            \
-                $(LOG)/HOL-Mirabelle.gz
+                $(LOG)/HOL-Mirabelle.gz $(LOG)/HOL-SMT.gz