# HG changeset patch
# User wenzelm
# Date 938549825 -7200
# Node ID 68e155f81f88354582437e1ae8cd0e298679d49e
# Parent  8e177a4c86a51971b2ec58cd981ff5707aa1961d
tuned;

diff -r 8e177a4c86a5 -r 68e155f81f88 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Sep 28 16:44:22 1999 +0200
+++ b/src/HOL/IsaMakefile	Tue Sep 28 22:17:05 1999 +0200
@@ -268,9 +268,10 @@
   MiniML/ROOT.ML MiniML/Type.ML MiniML/Type.thy MiniML/W.ML MiniML/W.thy
 	@$(ISATOOL) usedir $(OUT)/HOL MiniML
 
+
 ## HOL-BCV
 
-HOL-BCV:HOL $(LOG)/HOL-BCV.gz
+HOL-BCV: HOL $(LOG)/HOL-BCV.gz
 
 $(LOG)/HOL-BCV.gz: $(OUT)/HOL BCV/DFAandWTI.ML \
   BCV/DFAandWTI.thy BCV/DFAimpl.ML BCV/DFAimpl.thy \
@@ -433,5 +434,5 @@
 	  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \
 	  $(LOG)/HOL-ex.gz $(LOG)/HOL-Isar_examples.gz $(OUT)/TLA \
 	  $(LOG)/TLA.gz $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
-	  $(LOG)/TLA-Memory.gz $(LOG)/HOL-Real-ex.gz \
+	  $(LOG)/TLA-Memory.gz $(LOG)/HOL-Real.gz $(LOG)/HOL-Real-ex.gz \
 	  $(LOG)/HOL-Real-HahnBanach.gz