removed Lambda/Type.ML;

better rules for cancellation of common factors across comparisons

fixed a proof that had stopped working ???

tidied & updated proofs, deleting some unused ones

modified proofs: better rules for cancellation of common factors across comparisons

better rules for cancellation of common factors across comparisons

*** empty log message ***

cases: opaque by default; fixed ML tactic: proper context; added 'rename_tac', 'rename_tac';

renamed 'RS' to 'THEN';

tuned error handling;

added 'symmetric' attribute;

updated; tuned;

sel_upd proc: include 'more' pseudo-field; added equality rule;

renamed 'mk_cases_tac' to 'ind_cases';

changed 'opaque' option to 'open' (opaque is default); renamed 'mk_cases_tac' to 'ind_cases';

renamed 'RS' to 'THEN'; 'symmetric' attribute;

converted to new-style theory;

done;

'symmetric' attribute;

fixed deps;

renamed 'RS' to 'THEN';

index tokens; added 'int';

cases/induct method: 'opaque' by default; added 'open' option;

updated;

renamed 'RS' to 'THEN'; added 'rename_tac', 'rotate_tac'; added 'subst', 'hypsubst', and 'symmetric';

fixed lbrace, rbrace;

Isar/Pure: renamed 'RS' attribute to 'THEN'; Isar/Provers: added 'arith_split' attribute; Isar/Provers: added 'fastsimp' and 'clarsimp' methods; Isar/HOL/inductive: rename "intrs" to "intros"; HOL/record: added general record equality rule to simpset;

Fixed completeness bug in simplifier: congruence rules could preclude rewrites of the partially applied constant.

major sharpening of stable_project_transient

new (unused) lemma

new thm and simprule Compl_Diff_eq

added conversion.tex;