--- a/src/HOL/IsaMakefile Fri Apr 03 12:34:33 1998 +0200
+++ b/src/HOL/IsaMakefile Fri Apr 03 12:35:27 1998 +0200
@@ -9,7 +9,7 @@
default: HOL
images: HOL TLA
test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex HOL-Integ \
- HOL-Auth HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-IOA \
+ HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-IOA \
HOL-AxClasses HOL-AxClasses-Group HOL-AxClasses-Lattice \
HOL-AxClasses-Tutorial HOL-Quot HOL-ex TLA-Inc TLA-Buffer TLA-Memory
all: images test
@@ -140,6 +140,21 @@
@$(ISATOOL) usedir $(OUT)/HOL Auth
+## HOL-UNITY
+
+HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
+
+$(LOG)/HOL-UNITY.gz: $(OUT)/HOL UNITY/ROOT.ML\
+ UNITY/Channel.ML UNITY/Channel.thy UNITY/Common.ML UNITY/Common.thy\
+ UNITY/Deadlock.ML UNITY/Deadlock.thy UNITY/FP.ML UNITY/FP.thy\
+ UNITY/LessThan.ML UNITY/LessThan.thy UNITY/Mutex.ML UNITY/Mutex.thy\
+ UNITY/Network.ML UNITY/Network.thy UNITY/Reach.ML UNITY/Reach.thy\
+ UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/Token.ML UNITY/Token.thy\
+ UNITY/Traces.ML UNITY/Traces.thy UNITY/UNITY.ML UNITY/UNITY.thy\
+ UNITY/Update.ML UNITY/Update.thy UNITY/WFair.ML UNITY/WFair.thy
+ @$(ISATOOL) usedir $(OUT)/HOL UNITY
+
+
## HOL-Modelcheck
HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz
@@ -316,7 +331,8 @@
clean:
@rm -f $(OUT)/HOL $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
$(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \
- $(LOG)/HOL-Lex.gz $(LOG)/HOL-Integ.gz $(LOG)/HOL-Auth.gz \
+ $(LOG)/HOL-Lex.gz $(LOG)/HOL-Integ.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-AxClasses.gz \
$(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \