src/HOL/IsaMakefile
changeset 5605 e86700ddc7d4
parent 5564 f16de69b7c0c
child 5616 497eeeace3fc
equal deleted inserted replaced
5604:cd17004d09e1 5605:e86700ddc7d4
    28 
    28 
    29 Pure:
    29 Pure:
    30 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
    30 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
    31 
    31 
    32 $(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/cancel_sums.ML \
    32 $(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/cancel_sums.ML \
    33   $(SRC)/Provers/Arith/nat_transitive.ML $(SRC)/Provers/blast.ML \
    33   $(SRC)/Provers/Arith/nat_transitive.ML \
       
    34   $(SRC)/Provers/Arith/abel_cancel.ML $(SRC)/Provers/blast.ML \
    34   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
    35   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
    35   $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
    36   $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
    36   $(SRC)/Provers/splitter.ML $(SRC)/Pure/section_utils.ML \
    37   $(SRC)/Provers/splitter.ML $(SRC)/Pure/section_utils.ML \
    37   $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.new.sml \
    38   $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.new.sml \
    38   $(SRC)/TFL/rules.sig $(SRC)/TFL/sys.sml $(SRC)/TFL/tfl.sig \
    39   $(SRC)/TFL/rules.sig $(SRC)/TFL/sys.sml $(SRC)/TFL/tfl.sig \
   131 
   132 
   132 $(LOG)/HOL-Real.gz: $(OUT)/HOL \
   133 $(LOG)/HOL-Real.gz: $(OUT)/HOL \
   133   Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \
   134   Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \
   134   Real/PRat.ML Real/PRat.thy Real/PReal.ML Real/PReal.thy \
   135   Real/PRat.ML Real/PRat.thy Real/PReal.ML Real/PReal.thy \
   135   Real/RComplete.ML Real/RComplete.thy Real/Real.ML Real/Real.thy \
   136   Real/RComplete.ML Real/RComplete.thy Real/Real.ML Real/Real.thy \
       
   137   Real/RealDef.ML Real/RealDef.thy Real/simproc.ML \
   136   Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML
   138   Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML
   137 	@$(ISATOOL) usedir $(OUT)/HOL Real
   139 	@$(ISATOOL) usedir $(OUT)/HOL Real
   138 
   140 
   139 
   141 
   140 ## HOL-Auth
   142 ## HOL-Auth