src/HOL/IsaMakefile
changeset 8677 de62440762b8
parent 8569 748a9699f28d
child 8736 0bfd6678a5fa
equal deleted inserted replaced
8676:4bf18b611a75 8677:de62440762b8
   435 
   435 
   436 $(LOG)/HOL-Isar_examples.gz: $(OUT)/HOL Isar_examples/BasicLogic.thy \
   436 $(LOG)/HOL-Isar_examples.gz: $(OUT)/HOL Isar_examples/BasicLogic.thy \
   437   Isar_examples/Cantor.ML Isar_examples/Cantor.thy \
   437   Isar_examples/Cantor.ML Isar_examples/Cantor.thy \
   438   Isar_examples/ExprCompiler.thy Isar_examples/Fibonacci.thy \
   438   Isar_examples/ExprCompiler.thy Isar_examples/Fibonacci.thy \
   439   Isar_examples/Group.thy Isar_examples/KnasterTarski.thy \
   439   Isar_examples/Group.thy Isar_examples/KnasterTarski.thy \
   440   Isar_examples/MultisetOrder.thy \
   440   Isar_examples/MultisetOrder.thy		\
   441   Isar_examples/MutilatedCheckerboard.thy Isar_examples/Peirce.thy \
   441   Isar_examples/MutilatedCheckerboard.thy	\
       
   442   Isar_examples/NestedDatatype.thy Isar_examples/Peirce.thy \
   442   Isar_examples/Puzzle.thy Isar_examples/Summation.thy \
   443   Isar_examples/Puzzle.thy Isar_examples/Summation.thy \
   443   Isar_examples/ROOT.ML Isar_examples/W_correct.thy \
   444   Isar_examples/ROOT.ML Isar_examples/W_correct.thy \
   444   Isar_examples/document/proof.sty Isar_examples/document/root.bib \
   445   Isar_examples/document/proof.sty Isar_examples/document/root.bib \
   445   Isar_examples/document/root.tex Isar_examples/document/style.tex
   446   Isar_examples/document/root.tex Isar_examples/document/style.tex
   446 	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
   447 	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples