more markup;

simplify a proof due to 6c95a39348bd

new rule for making rsp theorem more readable

unregister lifting setup following the best practice of Lifting

generalised some results using type classes

More complex-related lemmas

the rules are not needed due to 1726f46d2aa8

simplify and repair proofs due to df0fda378813

rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user

Gauss.thy ported from Old_Number_Theory (unfinished)

merged

reverted c05d3e22adaf: Locale.intern is still required by AFP/Simpl;

optimize special case according to Library.merge (see also 8fbc355100f2, 520872460b7b);

tuned colors;

prefer standard Proof_Context.transfer, with theory stamp transfer (should now work thanks to purely functional theory, without Theory.copy etc.);

more robust registration of code equations

be consistent and produce always rep_eq with =

publish a useful function

don't be so aggresive for a public test function and raise only BAD_THM instead of ERROR

add missing attributes

Lemmas about Reals, norm, etc., and cleaner variants of existing ones

A few lemmas about summations, etc.

merged

tuned;

tuned messages -- prefer quote before Position.here, which might be just \<here>;

clarified ML language flags;

clarified painting of invisible caret, e.g. focus change due to popup;

tuned signature -- weaker type requirement;

paint completion range of active popup;

tuned messages;

clarified Token.range_of in accordance to Symbol_Pos.range; eliminated redundant Position.set_range, which is already included in Position.range;

tuned signature;

clarified interaction with dead variables in the composition of BNFs

added BNF cache (within one definition)

updated docs

optimized 'bnf_of_typ' further w.r.t. dead variables

optimization of 'bnf_of_typ' if all variables are dead

improved accounting for dead variables when naming set functions (refines d71c2737ee21)

added explicit killing

more precise error message

reuse same parser for '(co)datatype(_new)' as for 'bnf_decl'

tuned message;

tuned proofs;

tuned whitespace;

unused;

clarified semantic completion: retain kind.full_name as official item name for history; misc tuning;

try explicit semantic completion before syntax completion;

more explicit Completion.Item.range, independently of caret;

tuned whitespace;

clarified stretch_point_range wrt. UTF-16 surrogates; tuned;

tuned;

some rendering of completion range; tuned;

clarified completion names; tuned signature;

NEWS and documentation, including correction of long-overseen "*"

regenerated

keep only identifiers public which are explicitly requested or demanded by dependencies