updated subtle side-conditions;

some uses of 'obtain' with structure statement;

'obtain' supports structured statements (similar to 'define');

more portable: GNU find no longer supports "-perm +mode";

more uniform operations for structured statements;

defs are closed, which leads to proper auto_bind_facts; misc tuning;

tuned notation;

misc tuning and modernization;

Linear_Algebra: generalize linear_surjective_right/injective_left_inverse to real vector spaces

Linear_Algebra: generalize linear_independent_extend to all real vector spaces

Linear_Algebra: alternative representation of linear combination

Linear_Algebra: move abstract concepts to front

merge

avoid duplicate mixfix messages in '(co)datatype' type name

generalize code to avoid making assumptions about type variable names

intermediate definitions and caching in n2m to keep terms small

n2m operates on (un)folds

clarified rendering;

old 'def' is legacy;

more rigid check of lhs;

clarified def binding position: reset for implicit/derived binding, keep for explicit binding;

eliminated old 'def'; tuned comments;

added Isar command 'define';

within a proof body context, undeclared frees are like global constants; tuned signature;

clarified modules;

added "balanced" predicate

fixed code equation for pdivmod, added improved code equation for pseudo_mod

proper latex;

merged

reactivated other_id reports (see also db929027e701, 8eda56033203);