src/HOL/IsaMakefile
changeset 7627 6b0709a2f6c7
parent 7624 9024e9d370c7
child 7629 68e155f81f88
     1.1 --- a/src/HOL/IsaMakefile	Tue Sep 28 16:36:12 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Sep 28 16:37:04 1999 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  default: HOL
     1.5  images: HOL HOL-Real TLA
     1.6  test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex \
     1.7 -  HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML \
     1.8 +  HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-BCV \
     1.9    HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
    1.10    HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-ex \
    1.11    HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory
    1.12 @@ -268,6 +268,17 @@
    1.13    MiniML/ROOT.ML MiniML/Type.ML MiniML/Type.thy MiniML/W.ML MiniML/W.thy
    1.14  	@$(ISATOOL) usedir $(OUT)/HOL MiniML
    1.15  
    1.16 +## HOL-BCV
    1.17 +
    1.18 +HOL-BCV:HOL $(LOG)/HOL-BCV.gz
    1.19 +
    1.20 +$(LOG)/HOL-BCV.gz: $(OUT)/HOL BCV/DFAandWTI.ML \
    1.21 +  BCV/DFAandWTI.thy BCV/DFAimpl.ML BCV/DFAimpl.thy \
    1.22 +  BCV/Fixpoint.ML BCV/Fixpoint.thy BCV/Machine.ML BCV/Machine.thy \
    1.23 +  BCV/Orders.ML BCV/Orders.thy BCV/Orders0.ML BCV/Orders0.thy \
    1.24 +  BCV/Plus.ML BCV/Plus.thy BCV/ROOT.ML BCV/SemiLattice.ML BCV/SemiLattice.thy \
    1.25 +  BCV/Types0.ML BCV/Types0.thy BCV/Types.ML BCV/Types.thy
    1.26 +	@$(ISATOOL) usedir $(OUT)/HOL BCV
    1.27  
    1.28  ## HOL-IOA
    1.29  
    1.30 @@ -416,7 +427,7 @@
    1.31  	  $(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \
    1.32  	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    1.33  	  $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
    1.34 -	  $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz \
    1.35 +	  $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-BCV.gz $(LOG)/HOL-IOA.gz \
    1.36  	  $(LOG)/HOL-AxClasses-Group.gz		\
    1.37  	  $(LOG)/HOL-AxClasses-Lattice.gz	\
    1.38  	  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \