New simplifier flag for mutual simplification.

Removed expand_split from simpset.

removed pred;

eliminated pred function;

Symbol.explode;

replaced $LOGNAME by $USER;

tuned;

Symbol.is_*;

adapted to new scanner, baroque chars;

Symbol.input;

adapted to symbols, scan;

Generic scanners (for potentially infinite input) -- replaces Scanner;

adapted to new scanner and abroque chars;

read_var;

Symbol.output;

tuned syntax error msg;

Symbol.explode;

scan.ML, symbol.ML;

adapted to new scanners and baroque chars;

tuned some names;

adapted to baroque chars;

added merge_alists; moced is_letter etc. to Syntax/symbol.ML;

Syntax.indexname;

tuned comment;

tuned;

replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML; added Pure/Syntax/scan.ML;

replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;

Removed `addsplits [expand_if]'

added clasimp.ML;

Removed superfluous `op'

*** empty log message ***

Added delspilts, Addsplits, Delsplits.

expand_if is now by default part of the simpset.

New theorem and simprules

Reorganized simplifier. May now reorient rules. Moved loop tests from logic to thm.

Reorganized simplifier. May now reorient rules. This breaks many of the proofs in this file. Deactivated the feature locally.

Reorganized simplifier. May now reorient rules.

Better simplification allows deletion of parts of proofs

New theorem

New theorems

New theorems; tidied

New theorem diff_Suc_le_Suc_diff; tidied another proof

auto generated

Modified def.

Splitters via named loopers.

Little reorganization. Loop tactics have names now.

Tried to reorganize rewriter a little. More to be done.

added minimal description of rep_cs: corrections