added Quot examples;
authorwenzelm
Fri Apr 04 14:01:18 1997 +0200 (1997-04-04)
changeset 2900d5e1a2b869a2
parent 2899 c0abd2fd9b7c
child 2901 4e92704cf320
added Quot examples;
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Fri Apr 04 13:57:40 1997 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Apr 04 14:01:18 1997 +0200
     1.3 @@ -183,6 +183,14 @@
     1.4  	@$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial
     1.5  
     1.6  
     1.7 +## Higher-order quotients
     1.8 +
     1.9 +QUOT_FILES = Quot/ROOT.ML
    1.10 +
    1.11 +Quot:	$(OUT)/HOL $(QUOT_FILES)
    1.12 +	@$(ISATOOL) usedir $(OUT)/HOL Quot
    1.13 +
    1.14 +
    1.15  ## Miscellaneous examples
    1.16  
    1.17  EX_NAMES = String BT Perm Comb InSort Qsort LexProd \
    1.18 @@ -198,7 +206,7 @@
    1.19  ## Full test
    1.20  
    1.21  test:	$(OUT)/HOL \
    1.22 -	TFL IMP Hoare Lex Integ Auth Subst Lambda W0 MiniML IOA AxClasses ex
    1.23 +	TFL IMP Hoare Lex Integ Auth Subst Lambda W0 MiniML IOA AxClasses Quot ex
    1.24  	echo 'Test examples ran successfully' > test
    1.25  
    1.26