dropped dead code
Merge.
some updates on ancient README;
Simplifier already setup in Pure;
Transitivity reasoner renamed to linorder.ML. README updated.
HOL-Algebra partially ported to Isar.
induct_method.ML -- proof by cases and induction on sets and types (Isar);
updated
removed genelim.ML;
split_paired_all.ML: turn surjective pairing into split rule;
added clasimp.ML;
updated;
tuned;
tuned all READMEs;
added mention of simplifier, splitter, hypsubst
Initial revision