tuned;

some document antiquotations for Isabelle/jEdit elements; modernized theory setup;

merged

more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges; clarified sublocale_global: proper Local_Theory.exit (see also 8fe7414f00b1);

more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;

slightly more rubust (and opportunistic) exit for old-fashioned theory_to_proof, which is used by global 'sublocale' with Named_Target.init but without proper exit;

more standard internal data integrity;

tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;

tuned signature;

tuned comment;

minor performance tuning via fast matching filter;

added missing theorems to unfolding set

moved 'Quickcheck_Narrowing' further down the theory graph

make it possible to load Quickcheck exhaustive & narrowing in parallel

full path

measurable_lfp/gfp: indirection not necessary

merged

tuned proofs;

proper Char comparison, despite weakly-typed Scala (cf. 5ff5208de089);

tuned message;

tuned message;

include long identifiers in the reckoning of words (e.g. "integer.lifting" vs. 'lifting_update');

tuned messages -- in accordance to Isabelle/Scala;

tuned;

enabled test in PIDE interaction;

proper Args.syntax for slightly odd bundle trickery; do not handle arbitrary exceptions; more abstract type Args.src;

some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;

more markup;

clarified Args.check_src: retain name space information for error output; tuned signature;

tuned;

modernized data managed via Name_Space.table;

clarified Args.src: more abstract type, position refers to name only; prefer self-contained Args.check_src;

tuned signature;

prefer Name_Space.pretty with its builtin markup;

tuned signature -- prefer Name_Space.get with its builtin error;

abstract type Name_Space.table; clarified pretty_locale_deps: sort strings; clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;

more structured order;

more direct Long_Name.qualification;

more restrictive completion: intern/extern stability;

add measurability rule for (co)inductive predicates

introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices

hide implementation details

copy-paste typo

tuned tactic

unfold intermediate definitions after sealing the bnf

bootstrap fundamental Fun theory immediately after Set theory, without dependency on complete lattices * * * tuned

tuned; elimination rule subset_imageE; typical composition collapsing rewrite order in lemma image_image_eq_image_comp; destruction rules ball_imageD, bex_imageD

more careful unfolding of internal constants

made typedef for the type of the bound optional (size-based)

made natLe{q,ss} constants (yields smaller terms in composition)

removed junk

tuned proofs;

unused;

tuned;

more formal read_root;

simplified / modernized hide commands: proper outer parsers and PIDE markup via check;

removed dead code;

check fact names with PIDE markup;

tuned signature;

do allow replacement of words where this is appropriate, notably symbol abbrevs and keyword templates (see also 1c42ebdb3a58);