src/HOL/IsaMakefile
changeset 4777 379f32b0ae40
parent 4729 e1888c0d3b36
child 4830 bd73675adbed
     1.1 --- a/src/HOL/IsaMakefile	Fri Apr 03 12:34:33 1998 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Apr 03 12:35:27 1998 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  default: HOL
     1.5  images: HOL TLA
     1.6  test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex HOL-Integ \
     1.7 -  HOL-Auth HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-IOA \
     1.8 +  HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-IOA \
     1.9    HOL-AxClasses HOL-AxClasses-Group HOL-AxClasses-Lattice \
    1.10    HOL-AxClasses-Tutorial HOL-Quot HOL-ex TLA-Inc TLA-Buffer TLA-Memory
    1.11  all: images test
    1.12 @@ -140,6 +140,21 @@
    1.13  	@$(ISATOOL) usedir $(OUT)/HOL Auth
    1.14  
    1.15  
    1.16 +## HOL-UNITY
    1.17 +
    1.18 +HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
    1.19 +
    1.20 +$(LOG)/HOL-UNITY.gz: $(OUT)/HOL UNITY/ROOT.ML\
    1.21 +  UNITY/Channel.ML UNITY/Channel.thy UNITY/Common.ML UNITY/Common.thy\
    1.22 +  UNITY/Deadlock.ML UNITY/Deadlock.thy UNITY/FP.ML UNITY/FP.thy\
    1.23 +  UNITY/LessThan.ML UNITY/LessThan.thy UNITY/Mutex.ML UNITY/Mutex.thy\
    1.24 +  UNITY/Network.ML UNITY/Network.thy UNITY/Reach.ML UNITY/Reach.thy\
    1.25 +  UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/Token.ML UNITY/Token.thy\
    1.26 +  UNITY/Traces.ML UNITY/Traces.thy UNITY/UNITY.ML UNITY/UNITY.thy\
    1.27 +  UNITY/Update.ML UNITY/Update.thy UNITY/WFair.ML UNITY/WFair.thy
    1.28 +	@$(ISATOOL) usedir $(OUT)/HOL UNITY
    1.29 +
    1.30 +
    1.31  ## HOL-Modelcheck
    1.32  
    1.33  HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz
    1.34 @@ -316,7 +331,8 @@
    1.35  clean:
    1.36  	@rm -f $(OUT)/HOL $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
    1.37  	  $(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \
    1.38 -	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Integ.gz $(LOG)/HOL-Auth.gz \
    1.39 +	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Integ.gz \
    1.40 +	  $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    1.41  	  $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz \
    1.42  	  $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
    1.43  	  $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \