do less work in 'filter' mode

let exception pass through in debug mode

simplified preplaying information

renamed (hardly used) 'prod_pred' and 'option_pred' to 'pred_prod' and 'pred_option'

simplified solution parsing

adapted to renamed ML files

renamed ML files

reintroduced old model reconstruction code -- still needs to be ported

slacker error code policy for Z3

repaired 'if' logic

killed a few 'metis' calls

honor the fact that the new Z3 can generate Isar proofs

have Sledgehammer generate Isar proofs from Z3 proofs

tuned ML interface

integrate SMT2 with Sledgehammer

removed tracing output

use 'smt2' in SMT examples as much as currently possible

moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle

tuned proofs

dropped redundant theorems

tuned

monotonicity in complete lattices

enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions

tuned signature -- clarified module name;

added ML antiquotation @{here};

ML_Context.check_antiquotation still required;

simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser; added command 'print_ML_antiquotations';

proper base comparison;

tuned;

tuned proofs;

more explicit markup and explanation of the improper status of 'back', following the AFP style-guide;

clarified Markup.operator vs. Markup.delimiter; tuned color;

more explicit markup for Token.Literal; Markup.quasi_keyword for Parse.$$$ -- it is used within Args.syntax as well; Markup.operator for name of Args.syntax, to override outer keywords like "where"; tuned signature;

tuned signature;

modernized setup;

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);

tuned proofs;