src/HOL/IsaMakefile
changeset 33027 9cf389429f6d
parent 33026 8f35633c4922
child 33028 9aa8bfb1649d
     1.1 --- a/src/HOL/IsaMakefile	Tue Oct 20 19:37:09 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Oct 20 19:52:04 2009 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4    HOL-Lambda \
     1.5    HOL-Lattice \
     1.6    HOL-Matrix \
     1.7 -  HOL-MetisExamples \
     1.8 +  HOL-Metis_Examples \
     1.9    HOL-MicroJava \
    1.10    HOL-Mirabelle \
    1.11    HOL-Modelcheck \
    1.12 @@ -556,16 +556,16 @@
    1.13  	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hoare_Parallel
    1.14  
    1.15  
    1.16 -## HOL-MetisExamples
    1.17 +## HOL-Metis_Examples
    1.18  
    1.19 -HOL-MetisExamples: HOL $(LOG)/HOL-MetisExamples.gz
    1.20 +HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz
    1.21  
    1.22 -$(LOG)/HOL-MetisExamples.gz: $(OUT)/HOL MetisExamples/ROOT.ML	\
    1.23 -  MetisExamples/Abstraction.thy MetisExamples/BigO.thy		\
    1.24 -  MetisExamples/BT.thy MetisExamples/Message.thy		\
    1.25 -  MetisExamples/Tarski.thy MetisExamples/TransClosure.thy	\
    1.26 -  MetisExamples/set.thy
    1.27 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL MetisExamples
    1.28 +$(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML	\
    1.29 +  Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy	\
    1.30 +  Metis_Examples/BT.thy Metis_Examples/Message.thy		\
    1.31 +  Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy	\
    1.32 +  Metis_Examples/set.thy
    1.33 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples
    1.34  
    1.35  
    1.36  ## HOL-Algebra