equal inserted replaced
`     1 `
`     1                  Provers: generic theorem proving tools`
`     2                         Provers`
`       `
`     3 `
`     2 `
`     4 This directory contains ML sources of generic theorem proving tools.`
`     3 This directory contains ML sources of generic theorem proving tools.`
`     5 Typically, they can be applied to various logics, provided rules of a`
`     4 Typically, they can be applied to various logics, provided rules of a`
`     6 certain form are derivable.  Some of these are documented in the`
`     5 certain form are derivable.  Some of these are documented in the`
`     7 Reference Manual.`
`     6 Reference Manual.`
`     8 `
`     7 `
`     9 blast.ML                -- generic tableau prover with proof reconstruction`
`     8   blast.ML              generic tableau prover with proof reconstruction`
`    10 classical.ML            -- theorem prover for classical logics`
`     9   classical.ML          theorem prover for classical logics`
`    11 genelim.ML              -- bits and pieces for deriving elimination rules`
`    10   genelim.ML            bits and pieces for deriving elimination rules`
`    12 hypsubst.ML             -- tactic to substitute in the hypotheses`
`    11   hypsubst.ML           tactic to substitute in the hypotheses`
`    13 ind.ML                  -- a simple induction package`
`    12   ind.ML                a simple induction package`
`    14 simp.ML                 -- powerful but slow simplifier`
`    13   quantifier1.ML	simplification procedures for "1 point rules"`
`    15 simplifier.ML           -- fast simplifier`
`    14   simp.ML               powerful but slow simplifier`
`    16 splitter.ML             -- performs case splits for simplifier.ML`
`    15   simplifier.ML         fast simplifier`
`    17 typedsimp.ML            -- basic simplifier for explicitly typed logics`
`    16   splitter.ML           performs case splits for simplifier.ML`
`       `
`    17   typedsimp.ML          basic simplifier for explicitly typed logics`
`    18 `
`    18 `
`    19 directory Arith:`
`    19 directory Arith:`
`    20   nat_transitive.ML     -- simple package for inequalities over nat`
`    20   cancel_factor.ML	cancel common constant factor`
`    21 `
`    21   cancel_sums.ML	cancel common summands`
`    22 `
`    22   nat_transitive.ML	simple package for inequalities over nat`
`    23 \$Id\$`
`       `