src/HOL/IsaMakefile
changeset 10135 c2a4dccf6e67
parent 10094 22f201e9ec7a
child 10143 86c39bba873f
--- a/src/HOL/IsaMakefile	Tue Oct 03 18:30:56 2000 +0200
+++ b/src/HOL/IsaMakefile	Tue Oct 03 18:34:20 2000 +0200
@@ -8,13 +8,12 @@
 
 default: HOL
 images: HOL HOL-Real TLA
-test: HOL-Isar_examples HOL-Induct HOL-Lambda 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-AxClasses-Group HOL-AxClasses-Lattice \
-  HOL-AxClasses-Tutorial HOL-Real-ex \
-  HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory
+
+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
 
@@ -398,42 +397,13 @@
 	@$(ISATOOL) usedir $(OUT)/HOL IOA
 
 
-## HOL-AxClasses-Group
-
-HOL-AxClasses-Group: HOL $(LOG)/HOL-AxClasses-Group.gz
+## HOL-AxClasses
 
-$(LOG)/HOL-AxClasses-Group.gz: $(OUT)/HOL AxClasses/Group/Group.ML \
-  AxClasses/Group/Group.thy AxClasses/Group/GroupDefs.ML \
-  AxClasses/Group/GroupDefs.thy AxClasses/Group/GroupInsts.thy \
-  AxClasses/Group/Monoid.thy AxClasses/Group/MonoidGroupInsts.thy \
-  AxClasses/Group/ROOT.ML AxClasses/Group/Sigs.thy
-	@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group
-
-
-## HOL-AxClasses-Lattice
-
-HOL-AxClasses-Lattice: HOL $(LOG)/HOL-AxClasses-Lattice.gz
+HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz
 
-$(LOG)/HOL-AxClasses-Lattice.gz: $(OUT)/HOL AxClasses/Lattice/CLattice.ML \
-  AxClasses/Lattice/CLattice.thy AxClasses/Lattice/LatInsts.ML \
-  AxClasses/Lattice/LatInsts.thy AxClasses/Lattice/LatMorph.ML \
-  AxClasses/Lattice/LatMorph.thy AxClasses/Lattice/LatPreInsts.ML \
-  AxClasses/Lattice/LatPreInsts.thy AxClasses/Lattice/Lattice.ML \
-  AxClasses/Lattice/Lattice.thy AxClasses/Lattice/OrdDefs.ML \
-  AxClasses/Lattice/OrdDefs.thy AxClasses/Lattice/OrdInsts.thy \
-  AxClasses/Lattice/Order.ML AxClasses/Lattice/Order.thy \
-  AxClasses/Lattice/ROOT.ML
-	@$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice
-
-
-## HOL-AxClasses-Tutorial
-
-HOL-AxClasses-Tutorial: HOL $(LOG)/HOL-AxClasses-Tutorial.gz
-
-$(LOG)/HOL-AxClasses-Tutorial.gz: $(OUT)/HOL \
-  AxClasses/Tutorial/Group.thy AxClasses/Tutorial/Product.thy \
-  AxClasses/Tutorial/ROOT.ML AxClasses/Tutorial/Semigroups.thy
-	@$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial
+$(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/Group.thy \
+  AxClasses/Product.thy AxClasses/ROOT.ML AxClasses/Semigroups.thy
+	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
 
 
 ## HOL-ex
@@ -531,8 +501,7 @@
 		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
 		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
 		$(LOG)/HOL-BCV.gz $(LOG)/HOL-MicroJava.gz \
-		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses-Group.gz \
-		$(LOG)/HOL-AxClasses-Lattice.gz	\
-		$(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Real-ex.gz \
+		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
+		$(LOG)/HOL-Real-ex.gz \
 		$(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \
 		$(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz