updated;

open cases;

output \isachar;

cond_add_path;

fixed text;

turned into new-style theory;

tuned;

tuned \isastyle;

added \isachar definitions; added \isabellestyle switch; tuned;

%\urlstyle{rm} %\isabellestyle{it}

renamed cond_with_path to cond_add_path (add to front); improved with_path(s) (add to rear);

X-symbols for ordinal, cardinal, integer arithmetic

fixed RuleCases.make (invert flag);

removed obsolete add_recdef_x;

proper handling of defs;

Main now new-style theory; added Main.ML for compatibility;

simproc bug fix: only TYPING assumptions are given to the simplifier

better rules for cancellation of common factors across comparisons

new example ZF/ex/NatSum

now allows dest_coeff to fail

*** empty log message ***

*** empty log message ***

removed obsolete keyword;

fixed indexing;

tuned;

installed recdef congs data

added map_cong to recdef

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