HOL-Proofs is based in Main.thy
authorhaftmann
Wed, 02 Jun 2010 16:24:14 +0200
changeset 3729212a514e0319a
parent 37291 bc874e1a7758
child 37293 2c9ed7478e6e
HOL-Proofs is based in Main.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Wed Jun 02 16:24:13 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Jun 02 16:24:14 2010 +0200
     1.3 @@ -352,6 +352,9 @@
     1.4  $(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
     1.5  	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
     1.6  
     1.7 +$(OUT)/HOL-Proofs: main.ML $(MAIN_DEPENDENCIES)
     1.8 +	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs
     1.9 +
    1.10  HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
    1.11    Archimedean_Field.thy \
    1.12    Complex.thy \
    1.13 @@ -383,9 +386,6 @@
    1.14  $(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES)
    1.15  	@$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL
    1.16  
    1.17 -$(OUT)/HOL-Proofs: ROOT.ML $(HOL_DEPENDENCIES)
    1.18 -	@$(ISABELLE_TOOL) usedir -b -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs
    1.19 -
    1.20  
    1.21  
    1.22  ## HOL-Library