src/HOL/IsaMakefile
changeset 36649 bfd8c550faa6
parent 36648 43b66dcd9266
child 36700 9b85b9d74b83
--- a/src/HOL/IsaMakefile	Tue May 04 18:05:22 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue May 04 18:19:24 2010 +0200
@@ -1095,7 +1095,10 @@
   Multivariate_Analysis/Path_Connected.thy		\
   Multivariate_Analysis/Real_Integration.thy		\
   Multivariate_Analysis/Topology_Euclidean_Space.thy	\
-  Multivariate_Analysis/Vec1.thy
+  Multivariate_Analysis/Vec1.thy Library/Glbs.thy	\
+  Library/Inner_Product.thy Library/Numeral_Type.thy	\
+  Library/Convex.thy Library/FrechetDeriv.thy		\
+  Library/Product_Vector.thy Library/Product_plus.thy
 	@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-SMT HOL-Multivariate_Analysis
 
 
@@ -1109,7 +1112,10 @@
   Probability/Borel.thy Probability/Measure.thy			\
   Probability/Lebesgue.thy Probability/Product_Measure.thy	\
   Probability/Probability_Space.thy Probability/Information.thy \
-  Probability/ex/Dining_Cryptographers.thy
+  Probability/ex/Dining_Cryptographers.thy Library/FuncSet.thy	\
+  Library/Convex.thy Library/Product_Vector.thy 		\
+  Library/Product_plus.thy Library/Inner_Product.thy		\
+  Library/Nat_Bijection.thy
 	@cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Probability