src/HOL/IsaMakefile
changeset 3337 c056d328aa0e
parent 3294 4c73b6508f53
child 3354 3dac85693547
equal deleted inserted replaced
3336:29ddef80bd49 3337:c056d328aa0e
   198 	@$(ISATOOL) usedir $(OUT)/HOL Quot
   198 	@$(ISATOOL) usedir $(OUT)/HOL Quot
   199 
   199 
   200 
   200 
   201 ## Miscellaneous examples
   201 ## Miscellaneous examples
   202 
   202 
   203 EX_NAMES = Fib Primes NatSum String BT InSort Qsort Puzzle MT
   203 EX_NAMES = Fib Primes Primrec NatSum String BT InSort Qsort Puzzle MT
   204 
   204 
   205 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
   205 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
   206 	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   206 	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   207 
   207 
   208 ex:	$(OUT)/HOL $(EX_FILES)
   208 ex:	$(OUT)/HOL $(EX_FILES)