diff -r 02de0317f66f -r 73a0c804840f src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Oct 28 00:24:38 2009 +0100
+++ b/src/HOL/IsaMakefile	Wed Oct 28 11:43:06 2009 +0000
@@ -51,6 +51,7 @@
   HOL-Nominal-Examples \
   HOL-Number_Theory \
   HOL-Old_Number_Theory \
+  HOL-Probability \
   HOL-Prolog \
   HOL-SET_Protocol \
   HOL-SMT-Examples \
@@ -345,6 +346,7 @@
   RealVector.thy \
   SEQ.thy \
   Series.thy \
+  SupInf.thy \
   Taylor.thy \
   Transcendental.thy \
   Tools/float_syntax.ML \
@@ -1067,6 +1069,18 @@
   Multivariate_Analysis/Convex_Euclidean_Space.thy
 	@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis
 
+## HOL-Probability
+
+HOL-Probability: HOL $(LOG)/HOL-Probability.gz
+
+$(LOG)/HOL-Probability.gz: $(OUT)/HOL Probability/ROOT.ML \
+  Probability/Probability.thy \
+  Probability/Sigma_Algebra.thy \
+  Probability/SeriesPlus.thy \
+  Probability/Caratheodory.thy \
+  Probability/Measure.thy
+	$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Probability
+
 ## HOL-Nominal
 
 HOL-Nominal: HOL $(OUT)/HOL-Nominal