src/HOL/IsaMakefile
changeset 33262 b8d3b7196fe7
parent 33256 b350516cb1f9
parent 33249 2b65e9ed2e6e
child 33272 73a0c804840f
--- a/src/HOL/IsaMakefile	Tue Oct 27 16:47:27 2009 +0100
+++ b/src/HOL/IsaMakefile	Tue Oct 27 19:03:59 2009 +0100
@@ -1195,12 +1195,11 @@
 
 $(OUT)/HOL-SMT: $(OUT)/HOL-Word SMT/SMT_Base.thy SMT/Z3.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_proof_terms.ML SMT/Tools/z3_proof_rules.ML		\
-  SMT/Tools/z3_proof.ML SMT/Tools/z3_model.ML				\
-  SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML
+  SMT/Tools/smt_translate.ML SMT/Tools/smtlib_interface.ML              \
+  SMT/Tools/smt_solver.ML SMT/Tools/cvc3_solver.ML                      \
+  SMT/Tools/yices_solver.ML SMT/Tools/z3_proof_terms.ML                 \
+  SMT/Tools/z3_proof_rules.ML SMT/Tools/z3_proof.ML                     \
+  SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML
 	@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT