src/HOL/Makefile
changeset 1797 334308d2afbc
parent 1699 0bcc8cab3461
child 1862 74d4ae2f6fc3
equal deleted inserted replaced
1796:c42db9ab8728 1797:334308d2afbc
   179         then echo 'make_html := true; exit_use_dir"Lex";quit();' | $(LOGIC);\
   179         then echo 'make_html := true; exit_use_dir"Lex";quit();' | $(LOGIC);\
   180         else echo 'exit_use_dir"Lex";quit();' | $(LOGIC); \
   180         else echo 'exit_use_dir"Lex";quit();' | $(LOGIC); \
   181         fi
   181         fi
   182 
   182 
   183 ##Miscellaneous examples
   183 ##Miscellaneous examples
   184 EX_NAMES = LexProd MT Acc PropLog Puzzle Mutil Qsort LList Rec Simult Term \
   184 EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
   185 	   String BT Perm Comb
   185             Primes NatSum SList LList Acc PropLog Term Simult MT	    
   186 
   186 
   187 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
   187 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
   188            ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   188            ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   189 
   189 
   190 ex:     $(BIN)/HOL  $(EX_FILES)
   190 ex:     $(BIN)/HOL  $(EX_FILES)