--- a/src/HOL/IsaMakefile Mon Jul 31 12:33:26 2000 +0200
+++ b/src/HOL/IsaMakefile Mon Jul 31 12:50:33 2000 +0200
@@ -12,7 +12,7 @@
HOL-Hoare HOL-Lex HOL-Algebra HOL-Auth HOL-UNITY HOL-Modelcheck \
HOL-Lambda HOL-Prolog HOL-W0 HOL-MiniML HOL-BCV HOL-MicroJava \
HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
- HOL-AxClasses-Tutorial HOL-Quot HOL-Real-ex \
+ HOL-AxClasses-Tutorial HOL-Real-ex \
HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory
all: images test
@@ -411,16 +411,6 @@
@$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial
-## HOL-Quot
-
-HOL-Quot: HOL $(LOG)/HOL-Quot.gz
-
-$(LOG)/HOL-Quot.gz: $(OUT)/HOL Quot/FRACT.ML Quot/FRACT.thy \
- Quot/HQUOT.ML Quot/HQUOT.thy Quot/NPAIR.ML Quot/NPAIR.thy Quot/PER.ML \
- Quot/PER.thy Quot/PER0.ML Quot/PER0.thy Quot/ROOT.ML
- @$(ISATOOL) usedir $(OUT)/HOL Quot
-
-
## HOL-ex
HOL-ex: HOL $(LOG)/HOL-ex.gz