tuned;
authorwenzelm
Wed Nov 26 16:41:25 1997 +0100 (1997-11-26)
changeset 42895c1bfefd39b7
parent 4288 3f5e8c4aa84d
child 4290 902ee0883861
tuned;
src/HOL/IsaMakefile
src/Provers/README
     1.1 --- a/src/HOL/IsaMakefile	Wed Nov 26 16:38:04 1997 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Nov 26 16:41:25 1997 +0100
     1.3 @@ -13,17 +13,17 @@
     1.4  	Divides Power Sexp Univ List RelPow Option Map
     1.5  
     1.6  PROVERS = hypsubst.ML classical.ML blast.ML \
     1.7 -	simplifier.ML splitter.ML nat_transitive.ML 
     1.8 +	simplifier.ML splitter.ML Arith/nat_transitive.ML Arith/cancel_sums.ML
     1.9  
    1.10  TFL   = dcterm.sml post.sml rules.new.sml rules.sig \
    1.11  	sys.sml tfl.sig tfl.sml thms.sig thms.sml thry.sig thry.sml   \
    1.12  	usyntax.sig usyntax.sml utils.sig utils.sml
    1.13  
    1.14  FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \
    1.15 -	ind_syntax.ML cladata.ML simpdata.ML \
    1.16 -	typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML \
    1.17 +	ind_syntax.ML cladata.ML simpdata.ML arith_data.ML \
    1.18 +	typedef.ML thy_syntax.ML thy_data.ML $(ISABELLE_HOME)/src/Pure/section_utils.ML \
    1.19  	$(NAMES:%=%.thy) $(NAMES:%=%.ML) $(TFL:%=../TFL/%) \
    1.20 -	$(PROVERS:%=../Provers/%)
    1.21 +	$(PROVERS:%=$(ISABELLE_HOME)/src/Provers/%)
    1.22  
    1.23  $(OUT)/HOL: $(OUT)/Pure $(FILES)
    1.24  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
     2.1 --- a/src/Provers/README	Wed Nov 26 16:38:04 1997 +0100
     2.2 +++ b/src/Provers/README	Wed Nov 26 16:41:25 1997 +0100
     2.3 @@ -1,17 +1,23 @@
     2.4 -			Provers
     2.5 +
     2.6 +                        Provers
     2.7  
     2.8  This directory contains ML sources of generic theorem proving tools.
     2.9  Typically, they can be applied to various logics, provided rules of a
    2.10  certain form are derivable.  Some of these are documented in the
    2.11  Reference Manual.
    2.12  
    2.13 -blast.ML          -- generic tableau prover with proof reconstruction
    2.14 -classical.ML      -- theorem prover for classical logics
    2.15 -genelim.ML        -- bits and pieces for deriving elimination rules
    2.16 -hypsubst.ML       -- tactic to substitute in the hypotheses
    2.17 -ind.ML            -- a simple induction package
    2.18 -nat_transitive.ML -- simple package for inequalities over nat
    2.19 -simp.ML           -- powerful but slow simplifier
    2.20 -simplifier.ML     -- fast simplifier
    2.21 -splitter.ML       -- performs case splits for simplifier.ML
    2.22 -typedsimp.ML      -- basic simplifier for explicitly typed logics
    2.23 +blast.ML                -- generic tableau prover with proof reconstruction
    2.24 +classical.ML            -- theorem prover for classical logics
    2.25 +genelim.ML              -- bits and pieces for deriving elimination rules
    2.26 +hypsubst.ML             -- tactic to substitute in the hypotheses
    2.27 +ind.ML                  -- a simple induction package
    2.28 +simp.ML                 -- powerful but slow simplifier
    2.29 +simplifier.ML           -- fast simplifier
    2.30 +splitter.ML             -- performs case splits for simplifier.ML
    2.31 +typedsimp.ML            -- basic simplifier for explicitly typed logics
    2.32 +
    2.33 +directory Arith:
    2.34 +  nat_transitive.ML     -- simple package for inequalities over nat
    2.35 +
    2.36 +
    2.37 +$Id$