src/HOL/IsaMakefile
changeset 43162 9a8acc5adfa3
parent 43158 686fa0a0696e
child 43197 c71657bbdbc0
equal deleted inserted replaced
43161:27dcda8fc89b 43162:9a8acc5adfa3
   708 $(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \
   708 $(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \
   709   Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \
   709   Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \
   710   Metis_Examples/BT.thy Metis_Examples/Clausify.thy \
   710   Metis_Examples/BT.thy Metis_Examples/Clausify.thy \
   711   Metis_Examples/HO_Reas.thy Metis_Examples/Message.thy \
   711   Metis_Examples/HO_Reas.thy Metis_Examples/Message.thy \
   712   Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy \
   712   Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy \
   713   Metis_Examples/set.thy
   713   Metis_Examples/Typings.thy Metis_Examples/set.thy
   714 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples
   714 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples
   715 
   715 
   716 
   716 
   717 ## HOL-Nitpick_Examples
   717 ## HOL-Nitpick_Examples
   718 
   718