--- a/src/HOL/IsaMakefile Fri Apr 04 13:57:40 1997 +0200
+++ b/src/HOL/IsaMakefile Fri Apr 04 14:01:18 1997 +0200
@@ -183,6 +183,14 @@
@$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial
+## Higher-order quotients
+
+QUOT_FILES = Quot/ROOT.ML
+
+Quot: $(OUT)/HOL $(QUOT_FILES)
+ @$(ISATOOL) usedir $(OUT)/HOL Quot
+
+
## Miscellaneous examples
EX_NAMES = String BT Perm Comb InSort Qsort LexProd \
@@ -198,7 +206,7 @@
## Full test
test: $(OUT)/HOL \
- TFL IMP Hoare Lex Integ Auth Subst Lambda W0 MiniML IOA AxClasses ex
+ TFL IMP Hoare Lex Integ Auth Subst Lambda W0 MiniML IOA AxClasses Quot ex
echo 'Test examples ran successfully' > test