src/HOL/IsaMakefile
changeset 6880 ce2b19e4402d
parent 6817 a42849eeb674
child 6905 9bc05ec3497b
equal deleted inserted replaced
6879:70f8c0c34b8d 6880:ce2b19e4402d
   329 HOL-Isar_examples: HOL $(LOG)/HOL-Isar_examples.gz
   329 HOL-Isar_examples: HOL $(LOG)/HOL-Isar_examples.gz
   330 
   330 
   331 $(LOG)/HOL-Isar_examples.gz: $(OUT)/HOL Isar_examples/BasicLogic.thy \
   331 $(LOG)/HOL-Isar_examples.gz: $(OUT)/HOL Isar_examples/BasicLogic.thy \
   332   Isar_examples/Cantor.ML Isar_examples/Cantor.thy \
   332   Isar_examples/Cantor.ML Isar_examples/Cantor.thy \
   333   Isar_examples/ExprCompiler.thy Isar_examples/Group.thy \
   333   Isar_examples/ExprCompiler.thy Isar_examples/Group.thy \
   334   Isar_examples/NatSum.thy Isar_examples/Peirce.thy Isar_examples/ROOT.ML
   334   Isar_examples/KnasterTarski.thy Isar_examples/NatSum.thy \
       
   335   Isar_examples/Peirce.thy Isar_examples/ROOT.ML
   335 	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
   336 	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
   336 
   337 
   337 
   338 
   338 ## TLA
   339 ## TLA
   339 
   340