src/HOL/IsaMakefile
changeset 7307 c065073cdb34
parent 7301 6d43d525facc
child 7334 a90fc1e5fb19
     1.1 --- a/src/HOL/IsaMakefile	Fri Aug 20 15:42:46 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Aug 20 15:43:25 1999 +0200
     1.3 @@ -9,8 +9,8 @@
     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 HOL-IOA \
     1.8 -  HOL-AxClasses HOL-AxClasses-Group HOL-AxClasses-Lattice \
     1.9 +  HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML \
    1.10 +  HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
    1.11    HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples TLA-Inc \
    1.12    TLA-Buffer TLA-Memory
    1.13  
    1.14 @@ -254,17 +254,9 @@
    1.15  	@$(ISATOOL) usedir $(OUT)/HOL IOA
    1.16  
    1.17  
    1.18 -## HOL-AxClasses
    1.19 -
    1.20 -HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz
    1.21 -
    1.22 -$(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/ROOT.ML
    1.23 -	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
    1.24 -
    1.25 -
    1.26  ## HOL-AxClasses-Group
    1.27  
    1.28 -HOL-AxClasses-Group: HOL-AxClasses $(LOG)/HOL-AxClasses-Group.gz
    1.29 +HOL-AxClasses-Group: HOL $(LOG)/HOL-AxClasses-Group.gz
    1.30  
    1.31  $(LOG)/HOL-AxClasses-Group.gz: $(OUT)/HOL AxClasses/Group/Group.ML \
    1.32    AxClasses/Group/Group.thy AxClasses/Group/GroupDefs.ML \
    1.33 @@ -276,7 +268,7 @@
    1.34  
    1.35  ## HOL-AxClasses-Lattice
    1.36  
    1.37 -HOL-AxClasses-Lattice: HOL-AxClasses $(LOG)/HOL-AxClasses-Lattice.gz
    1.38 +HOL-AxClasses-Lattice: HOL $(LOG)/HOL-AxClasses-Lattice.gz
    1.39  
    1.40  $(LOG)/HOL-AxClasses-Lattice.gz: $(OUT)/HOL AxClasses/Lattice/CLattice.ML \
    1.41    AxClasses/Lattice/CLattice.thy AxClasses/Lattice/LatInsts.ML \
    1.42 @@ -292,7 +284,7 @@
    1.43  
    1.44  ## HOL-AxClasses-Tutorial
    1.45  
    1.46 -HOL-AxClasses-Tutorial: HOL-AxClasses $(LOG)/HOL-AxClasses-Tutorial.gz
    1.47 +HOL-AxClasses-Tutorial: HOL $(LOG)/HOL-AxClasses-Tutorial.gz
    1.48  
    1.49  $(LOG)/HOL-AxClasses-Tutorial.gz: $(OUT)/HOL \
    1.50    AxClasses/Tutorial/BoolGroupInsts.thy AxClasses/Tutorial/Group.ML \
    1.51 @@ -398,9 +390,10 @@
    1.52  	@rm -f $(OUT)/HOL $(OUT)/HOL-Real $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
    1.53  	  $(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \
    1.54  	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    1.55 -	  $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz \
    1.56 -	  $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
    1.57 -	  $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \
    1.58 +	  $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
    1.59 +	  $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz \
    1.60 +	  $(LOG)/HOL-AxClasses-Group.gz		\
    1.61 +	  $(LOG)/HOL-AxClasses-Lattice.gz	\
    1.62  	  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \
    1.63  	  $(LOG)/HOL-ex.gz $(LOG)/HOL-Isar_examples.gz $(OUT)/TLA \
    1.64  	  $(LOG)/TLA.gz $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \