Added Example Quot
authorslotosch
Fri, 04 Apr 1997 16:04:28 +0200
changeset 2909 22a8a97b66be
parent 2908 b9ba893e72cd
child 2910 905aa895136c
Added Example Quot CVS ----------------------------------------------------------------------
src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Apr 04 16:03:48 1997 +0200
+++ b/src/HOL/IsaMakefile	Fri Apr 04 16:04:28 1997 +0200
@@ -183,10 +183,11 @@
 	@$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial
 
 
-## Higher-order quotients
+## Higher-order quotients and example fractionals
 
-QUOT_FILES = Quot/ROOT.ML
-
+QUOT_FILES = Quot/ROOT.ML Quot/PER0.thy Quot/PER0.ML Quot/PER.thy Quot/PER.ML \
+	Quot/HQUOT.thy Quot/HQUOT.ML Quot/NPAIR.thy Quot/NPAIR.ML \
+	Quot/FRACT.thy Quot/FRACT.ML
 Quot:	$(OUT)/HOL $(QUOT_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOL Quot