optimize special case according to Library.merge (see also 8fbc355100f2); no treatment for Net.merge, due to non-standard merge order;

more positions; tuned messages;

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

explicit option for "open" code generation

tuned

more fine-grain notion of export

tuned

formal markup for public ingredients

tuned

dropped long-unused option

avoid ad-hoc patching of generated code

tuned proofs;

support for semantic completion on Scala side;

clarified module location (again, see 763d35697338);

support for completion within the formal context; tuned signature;

removed remains of old experiment (see b933142e02d0);

removed dead code; more complete patterns;

tuned signature;

NEWS;

tuned comment;

refined language context: antiquotes; support default completions, with move of caret position; tuned signature;

tuned proofs;

merged

more standard theory name;

tuned;

tuned whitespace; tuned names;

proper ML structure with signature;

reduced ML warnings;

simultaneous mapping of strongly connected components

dropped dead code

more symbols;

merged

improved completion based on context information;

more markup -- complete symbols within antiquotation, notably with broken arguments;

eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);

tuned signature -- avoid redundancy and confusion of flags;

tuned signature;

more general / abstract Command.Markups, with separate index for status elements; slightly faster Rendering.overview_color;

tuned signature -- avoid obscure default arguments;

more lightweight Rendering;

tuned signature;

tuned -- remaining rev_markup is rather short after filter;

only one internal coinduction rule

NEWS

adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'

renamed 'recs' and 'cases' theorems 'rec' and 'case' in old datatype package, for consistency with new package

tuned proofs; more symbols;

tuned whitespace;

updated keywords;

merged

more official params in context;

tuned signature; tuned message;

tuned messages; more official hyps;

clarified printing of undeclared hyps;

modernized tool setup; tuned;

removed dead code;

tuned;

proper naming convention;

prefer cat_lines;

tuned whitespace;

tuned comments;

complete symbols within ML strings / comments;

tuned messages;

tuned;

clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;