fixing ennreal using add_mono1; shifting results from linordered_semidom to linordered_nonzero_semiring

merged

type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0

simplified Radix_Sort

merged

merged

moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations

simplified def of stable

Lots of new material about matrices, etc.

tuned proofs -- prefer explicit names for facts from 'interpret';

merged

eliminated questionable Par_List.map -- locale interpretation is mostly lazy (see also b81f1de9f57e);

tuned signature;

tuned;

use lazy notes for locale context init and later additions of facts;

avoid premature Lazy.force due to strict "?" operator;

Merge

Merge

lots of new material, ultimately related to measure theory

merged

support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes; register_proofs is now based on lazy thms, but Thm.consolidate_theory will eventually force this (in parallel); support for lazy notes for locale activation (still inactive);

tuned;

tuned: more parallel;

clarified modules;

clarified modules;

tuned;

tuned;

tuned signature;