# HG changeset patch
# User nipkow
# Date 938529424 -7200
# Node ID 6b0709a2f6c7a4799962287fad72b5dbc80be6fe
# Parent  5997f35954d76f4d41b67cf5922848a1385de194
added BCV.

diff -r 5997f35954d7 -r 6b0709a2f6c7 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Sep 28 16:36:12 1999 +0200
+++ b/src/HOL/IsaMakefile	Tue Sep 28 16:37:04 1999 +0200
@@ -9,7 +9,7 @@
 default: HOL
 images: HOL HOL-Real TLA
 test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex \
-  HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML \
+  HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-BCV \
   HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
   HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-ex \
   HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory
@@ -268,6 +268,17 @@
   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
+
+$(LOG)/HOL-BCV.gz: $(OUT)/HOL BCV/DFAandWTI.ML \
+  BCV/DFAandWTI.thy BCV/DFAimpl.ML BCV/DFAimpl.thy \
+  BCV/Fixpoint.ML BCV/Fixpoint.thy BCV/Machine.ML BCV/Machine.thy \
+  BCV/Orders.ML BCV/Orders.thy BCV/Orders0.ML BCV/Orders0.thy \
+  BCV/Plus.ML BCV/Plus.thy BCV/ROOT.ML BCV/SemiLattice.ML BCV/SemiLattice.thy \
+  BCV/Types0.ML BCV/Types0.thy BCV/Types.ML BCV/Types.thy
+	@$(ISATOOL) usedir $(OUT)/HOL BCV
 
 ## HOL-IOA
 
@@ -416,7 +427,7 @@
 	  $(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \
 	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
 	  $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
-	  $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz \
+	  $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-BCV.gz $(LOG)/HOL-IOA.gz \
 	  $(LOG)/HOL-AxClasses-Group.gz		\
 	  $(LOG)/HOL-AxClasses-Lattice.gz	\
 	  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \