src/HOL/IsaMakefile
changeset 32496 4ab00a2642c3
parent 32479 521cc9bf2958
child 32500 7106aeb6dd64
     1.1 --- a/src/HOL/IsaMakefile	Wed Sep 02 16:02:37 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Sep 02 16:23:53 2009 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4    HOL-Matrix \
     1.5    HOL-MetisExamples \
     1.6    HOL-MicroJava \
     1.7 +  HOL-Mirabelle \
     1.8    HOL-Modelcheck \
     1.9    HOL-NanoJava \
    1.10    HOL-Nominal-Examples \
    1.11 @@ -1119,6 +1120,20 @@
    1.12  	@cd NSA; $(ISABELLE_TOOL) usedir $(OUT)/HOL-NSA Examples
    1.13  
    1.14  
    1.15 +## HOL-Mirabelle
    1.16 +
    1.17 +HOL-Mirabelle: HOL $(LOG)/HOL-Mirabelle.gz
    1.18 +
    1.19 +$(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/MirabelleTest.thy \
    1.20 +  Mirabelle/Mirabelle.thy Mirabelle/Tools/mirabelle.ML Mirabelle/ROOT.ML \
    1.21 +  Mirabelle/Tools/mirabelle_arith.ML \
    1.22 +  Mirabelle/Tools/mirabelle_metis.ML \
    1.23 +  Mirabelle/Tools/mirabelle_quickcheck.ML \
    1.24 +  Mirabelle/Tools/mirabelle_refute.ML \
    1.25 +  Mirabelle/Tools/mirabelle_sledgehammer.ML
    1.26 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
    1.27 +
    1.28 +
    1.29  ## clean
    1.30  
    1.31  clean:
    1.32 @@ -1140,4 +1155,5 @@
    1.33  		$(LOG)/TLA-Memory.gz $(LOG)/HOL-Library.gz		\
    1.34  		$(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz	\
    1.35  		$(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA		\
    1.36 -		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz
    1.37 +		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz            \
    1.38 +                $(LOG)/HOL-Mirabelle.gz