# HG changeset patch
# User nipkow
# Date 991983008 -7200
# Node ID 2511e48c532449ff393b39d20ed3c3a07b5b6c19
# Parent  879e53d92f51a4b070af82e629567050dca62194
Removed BCV

diff -r 879e53d92f51 -r 2511e48c5324 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jun 05 09:51:04 2001 +0200
+++ b/src/HOL/IsaMakefile	Fri Jun 08 08:50:08 2001 +0200
@@ -15,7 +15,6 @@
   HOL-Algebra \
   HOL-Auth \
   HOL-AxClasses \
-  HOL-BCV \
   HOL-CTL \
       HOL-Real-HahnBanach \
       HOL-Real-ex \
@@ -448,19 +447,6 @@
 	@$(ISATOOL) usedir $(OUT)/HOL MicroJava
 
 
-## HOL-BCV
-
-HOL-BCV: HOL $(LOG)/HOL-BCV.gz
-
-$(LOG)/HOL-BCV.gz: $(OUT)/HOL \
-  BCV/DFA_Framework.thy BCV/DFA_Framework.ML BCV/Err.thy BCV/Err.ML \
-  BCV/JType.ML BCV/JType.thy BCV/JVM.ML BCV/JVM.thy \
-  BCV/Kildall.ML BCV/Kildall.thy BCV/Listn.ML BCV/Listn.thy \
-  BCV/Opt.ML BCV/Opt.thy BCV/ROOT.ML BCV/Semilat.ML BCV/Semilat.thy \
-  BCV/Product.ML BCV/Product.thy
-	@$(ISATOOL) usedir $(OUT)/HOL BCV
-
-
 ## HOL-CTL
 
 HOL-CTL: HOL $(LOG)/HOL-CTL.gz
@@ -590,7 +576,7 @@
 		$(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-BCV.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-MicroJava.gz \
+		$(LOG)/HOL-CTL.gz $(LOG)/HOL-MicroJava.gz \
 		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
 		$(LOG)/HOL-Lattice $(LOG)/HOL-Real-ex.gz \
 		$(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \