src/HOL/IsaMakefile
changeset 10157 6d3987f3aad9
parent 10143 86c39bba873f
child 10212 33fe2d701ddd
--- a/src/HOL/IsaMakefile	Thu Oct 05 14:04:56 2000 +0200
+++ b/src/HOL/IsaMakefile	Fri Oct 06 01:04:56 2000 +0200
@@ -9,13 +9,38 @@
 default: HOL
 images: HOL HOL-Real TLA
 
-test: HOL-Isar_examples HOL-Induct HOL-Lambda HOL-AxClasses HOL-ex HOL-Subst HOL-IMP \
-  HOL-IMPP HOL-NumberTheory HOL-Hoare HOL-Lex HOL-Algebra HOL-Auth \
-  HOL-UNITY HOL-Modelcheck HOL-Prolog HOL-W0 HOL-MiniML HOL-BCV \
-  HOL-MicroJava HOL-IOA HOL-Real-ex HOL-Real-HahnBanach \
-  TLA-Inc TLA-Buffer TLA-Memory
-
-all: images test
+#Note: keep targets sorted!
+test: \
+  HOL-Algebra \
+  HOL-Auth \
+  HOL-AxClasses \
+  HOL-BCV \
+      HOL-Real-HahnBanach \
+      HOL-Real-ex \
+  HOL-Hoare \
+  HOL-IMP \
+  HOL-IMPP \
+  HOL-IOA \
+  HOL-Induct \
+  HOL-Isar_examples \
+  HOL-Lambda \
+  HOL-Lattice \
+  HOL-Lex \
+  HOL-MicroJava \
+  HOL-MiniML \
+  HOL-Modelcheck \
+  HOL-NumberTheory \
+  HOL-Prolog \
+  HOL-Subst \
+      TLA-Buffer \
+      TLA-Inc \
+      TLA-Memory \
+  HOL-UNITY \
+  HOL-W0 \
+  HOL-ex
+    # ^ this is the sort position
+  
+all: test images
 
 
 ## global settings
@@ -406,6 +431,16 @@
 	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
 
 
+## HOL-Lattice
+
+HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
+
+$(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy \
+  Lattice/CompleteLattice.thy Lattice/Lattice.thy Lattice/Orders.thy \
+  Lattice/ROOT.ML Lattice/document/root.tex
+	@$(ISATOOL) usedir $(OUT)/HOL Lattice
+
+
 ## HOL-ex
 
 HOL-ex: HOL $(LOG)/HOL-ex.gz
@@ -502,6 +537,6 @@
 		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
 		$(LOG)/HOL-BCV.gz $(LOG)/HOL-MicroJava.gz \
 		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
-		$(LOG)/HOL-Real-ex.gz \
+		$(LOG)/HOL-Lattice $(LOG)/HOL-Real-ex.gz \
 		$(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \
 		$(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz