src/HOL/IsaMakefile
changeset 35957 ed52ade112c0
parent 35956 f53dc0b539fa
parent 35944 c53a6865111b
child 35959 b88e061754a1
--- a/src/HOL/IsaMakefile	Wed Mar 24 17:40:44 2010 +0100
+++ b/src/HOL/IsaMakefile	Wed Mar 24 17:41:25 2010 +0100
@@ -1078,7 +1078,10 @@
   Multivariate_Analysis/Topology_Euclidean_Space.thy	\
   Multivariate_Analysis/Convex_Euclidean_Space.thy      \
   Multivariate_Analysis/Brouwer_Fixpoint.thy            \
-  Multivariate_Analysis/Derivative.thy
+  Multivariate_Analysis/Derivative.thy			\
+  Multivariate_Analysis/Integration.thy			\
+  Multivariate_Analysis/Integration.cert		\
+  Multivariate_Analysis/Real_Integration.thy
 	@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-SMT HOL-Multivariate_Analysis
 
 
@@ -1228,7 +1231,7 @@
   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 $(SRC)/Tools/Cache_IO/cache_io.ML
+  SMT/Tools/z3_solver.ML $(SRC)/Tools/cache_io.ML
 	@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT