src/HOL/IsaMakefile
changeset 23449 dd874e6a3282
parent 23445 6908c13215d1
child 23454 c54975167be9
     1.1 --- a/src/HOL/IsaMakefile	Thu Jun 21 12:01:27 2007 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Jun 21 13:23:33 2007 +0200
     1.3 @@ -27,6 +27,7 @@
     1.4    HOL-Isar_examples \
     1.5    HOL-Lambda \
     1.6    HOL-Lattice \
     1.7 +  HOL-MetisExamples \
     1.8    HOL-MicroJava \
     1.9    HOL-Modelcheck \
    1.10    HOL-NanoJava \
    1.11 @@ -390,6 +391,18 @@
    1.12  	@$(ISATOOL) usedir -g true $(OUT)/HOL HoareParallel
    1.13  
    1.14  
    1.15 +## HOL-MetisExamples
    1.16 +
    1.17 +HOL-MetisExamples: HOL $(LOG)/HOL-MetisExamples.gz
    1.18 +
    1.19 +$(LOG)/HOL-MetisExamples.gz: $(OUT)/HOL \
    1.20 +  MetisExamples/ROOT.ML \
    1.21 +  MetisExamples/Abstraction.thy MetisExamples/BigO.thy MetisExamples/BT.thy \
    1.22 +  MetisExamples/Message.thy MetisExamples/Tarski.thy MetisExamples/TransClosure.thy \
    1.23 +  MetisExamples/set.thy
    1.24 +	@$(ISATOOL) usedir -g true $(OUT)/HOL MetisExamples
    1.25 +
    1.26 +
    1.27  ## HOL-Algebra
    1.28  
    1.29  HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz