# HG changeset patch
# User wenzelm
# Date 1269369333 -3600
# Node ID 5f38ae62d93940a867044cdd2abf4965c9804a69
# Parent  f135ebcc835c80ed35df34c4a343794ac842447e# Parent  6c9f7dc1ad07a1b5451d64c73c7ffc31cc9c8978
merged

diff -r f135ebcc835c -r 5f38ae62d939 Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makedist	Tue Mar 23 10:07:39 2010 -0700
+++ b/Admin/isatest/isatest-makedist	Tue Mar 23 19:35:33 2010 +0100
@@ -96,7 +96,7 @@
 sleep 15
 $SSH macbroy22 "$MAKEALL $HOME/settings/at-poly"
 sleep 15
-$SSH macbroy23 "$MAKEALL -l HOL HOL-ex $HOME/settings/at-sml-dev-e"
+$SSH macbroy23 "$MAKEALL -l HOL HOL-Library $HOME/settings/at-sml-dev-e"
 sleep 15
 $SSH macbroy24 "$MAKEALL $HOME/settings/at64-poly"
 sleep 15
diff -r f135ebcc835c -r 5f38ae62d939 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Mar 23 10:07:39 2010 -0700
+++ b/src/HOL/IsaMakefile	Tue Mar 23 19:35:33 2010 +0100
@@ -10,13 +10,14 @@
 images: \
   HOL \
   HOL-Algebra \
+  HOL-Base \
   HOL-Boogie \
-  HOL-Base \
   HOL-Main \
   HOL-Multivariate_Analysis \
   HOL-NSA \
   HOL-Nominal \
   HOL-Plain \
+  HOL-Probability \
   HOL-Proofs \
   HOL-SMT \
   HOL-Word \
@@ -54,7 +55,6 @@
   HOL-Number_Theory \
   HOL-Old_Number_Theory \
   HOL-Quotient_Examples \
-  HOL-Probability \
   HOL-Prolog \
   HOL-Proofs-Extraction \
   HOL-Proofs-Lambda \
@@ -1084,17 +1084,13 @@
 
 ## HOL-Probability
 
-HOL-Probability: HOL $(LOG)/HOL-Probability.gz
+HOL-Probability: HOL $(OUT)/HOL-Probability
 
-$(LOG)/HOL-Probability.gz: $(OUT)/HOL Probability/ROOT.ML	\
-  Probability/Probability.thy					\
-  Probability/Sigma_Algebra.thy					\
-  Probability/SeriesPlus.thy					\
-  Probability/Caratheodory.thy					\
-  Probability/Borel.thy						\
-  Probability/Measure.thy					\
-  Probability/Lebesgue.thy					\
-  Probability/Product_Measure.thy				\
+$(OUT)/HOL-Probability: $(OUT)/HOL Probability/ROOT.ML		\
+  Probability/Probability.thy Probability/Sigma_Algebra.thy	\
+  Probability/SeriesPlus.thy Probability/Caratheodory.thy	\
+  Probability/Borel.thy Probability/Measure.thy			\
+  Probability/Lebesgue.thy Probability/Product_Measure.thy	\
   Probability/Probability_Space.thy
 	@cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Probability
 
@@ -1316,12 +1312,12 @@
 		$(LOG)/HOL-SMT-Examples.gz $(LOG)/HOL-SMT.gz		\
 		$(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz		\
 		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz			\
-		$(LOG)/HOL-Word-Examples.gz		\
-		$(LOG)/HOL-Word.gz $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz	\
-		$(LOG)/HOL.gz $(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz	\
-		$(LOG)/TLA-Inc.gz $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz	\
-		$(OUT)/HOL $(OUT)/HOL-Algebra $(OUT)/HOL-Base		\
-		$(OUT)/HOL-Boogie $(OUT)/HOL-Main			\
-		$(OUT)/HOL-Multivariate_Analysis $(OUT)/HOL-NSA		\
-		$(OUT)/HOL-Nominal $(OUT)/HOL-Plain $(OUT)/HOL-Proofs	\
+		$(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz		\
+		$(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz $(LOG)/HOL.gz		\
+		$(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz	\
+		$(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL		\
+		$(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie	\
+		$(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis	\
+		$(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain	\
+		$(OUT)/HOL-Probability $(OUT)/HOL-Proofs		\
 		$(OUT)/HOL-SMT $(OUT)/HOL-Word $(OUT)/HOL4 $(OUT)/TLA