Cancel common constant factor from balanced exression.

Cancel common summands of balanced expressions.

removed conv_prover;

tuned;

added crep_cterm;

fixed type of thms_containing;

added foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a; added foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a; added foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a;

cleaned signature; added instantiate': ctyp option list -> cterm option list -> thm -> thm;

removed merge_opts;

managed merge details;

resolved merge conflict;

Added read_def_cterms for simultaneous reading/typing of terms under defaults. Redefined read_def_cterm in in terms of read_def_cterms. Deleted obsolete read_cterms. Cleaned up def of read_insts, which is not much shorter but much clearere are correcter now.

fixed warning;

made SML/NJ happy;

tuned;

replaced by seq.ML;

changed Pure/Sequence interface;

SYNC;

cd, use: path variables;

comment;

obsolete;

changed Pure/Sequence interface -- isatool fixseq;

changed Sequence interface (now Seq, in seq.ML);

cd, use etc. now support path variables; changed Pure/Sequence interface;

fix references to obsolete Pure/Sequence structure;

tidying

analz_mono_contra_tac was wrong

Deleted some useless comments

minor improvements of formulation and proofs

corrected INDUCT_FILES

$ISABELLE_HOME/src;

improved error msg;