Updated proofs because of new simplification tactics.

Adapted proofs because of new simplification tactics.

The new asm_lr_simp_tac is the old asm_full_simp_tac. The new asm_full_simp_tac also does a limited amount of mutual simplification.

renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin

added not1_or and if_eq_cancel to simpset() renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin

added not1_or and if_eq_cancel to simpset()

new rewrite rules not1_or, not2_or, and if_eq_cancel added not1_or and if_eq_cancel to simpset()

renamed smart_tac to force_tac, slight improvement of force_tac

Asm_full_simp_tac now reorients asm c = t to t = c.

adhoc fix of is_blank;

New scanner in abstract form.

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;