# HG changeset patch
# User nipkow
# Date 965040633 -7200
# Node ID f3ab2f3c19a237409d713744d4df59d05ec434fb
# Parent  d7e354c16dc6bd89f9e577acea8643f325a2146b
Removed Quot

diff -r d7e354c16dc6 -r f3ab2f3c19a2 src/HOL/IsaMakefile
--- 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