tuned;

tuned signature;

tuned signature;

clarified key event propagation, in accordance to outer_key_listener;

allow implicit semantic completion, notably after delay that exceeds usual round-trip time; clarified isabelle.completion action: already open popup is re-opened and thus updated;

reject internal names, notably from Term.free_dummy_patterns;

more uniform alias vs. hide: proper check, allow to hide global names as well;

tuned proofs

normalising simp rules for compound operators

tuned markup;

minor tuning;

more markup;

clarified completion ordering: prefer local names;

tuned signature; eliminated clones;

tuned -- avoid vacuous reports;

clarified local facts;

more explicit treatment of verbose mode, which includes concealed entries;

removed dead code;

clarified retrieve_generic: local error takes precedence, which is relevant for completion;

clarified print_local_facts;

more complete set of lemmas wrt. image and composition

merge

add error messages for invalid inputs

add lemmas about nhds filter; tuned proof

remove unused lemma which was a direct consequence of tendsto_intros

merged

merged

prefer more robust Synchronized.var;

discontinued somewhat pointless "thy_script" keyword kind;

conceal improper cases, e.g. relevant for completion (and potentially for markup);

conceal somewhat obscure internal facts, e.g. relevant for 'print_theorems', 'find_theorems';

more accurate resolution of hybrid facts, which actually changes the sort order of results;

tuned -- command 'text' was localized some years ago;

back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;

just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.); more thorough background_notes: distribute global notes to all contexts;

more frugal recording of changes: join merely requires information from one side; tuned;

do not test details of error messages;

minor tuning -- NB: props are usually empty for global facts;

even smarter Path.smart_implode;

added ML antiquotation @{path};

clarified Path.smart_implode; more informative report and rendering;

generalization of differential_zero_maxmin to class real_normed_vector

delayed construction of command (and of noncommercial check) + tuning

tuning

consolidate consecutive steps that prove the same formula

remove '__' skolem suffixes before showing terms to users

undo rewrite rules (e.g. for 'fun_app') in Isar

debugging stuff

more simplification of trivial steps

tuning

tuned wording (pun)

document the new 'nonexhaustive' option (cf. 52e8f110fec3)

made SML/NJ happier

print warning if some constructors are missing; make this warning optional via "(nonexhaustive)"

updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'

updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit

updated NEWS and CONTRIBUTORS (BNF, SMT2, Sledgehammer)

remove ordered_euclidean_space constraint from brouwer/derivative lemmas; add constant unit_cube for class euclidean_space

typos

merged

tuned tactics

simplified internal codatatype construction

updated SMT2 examples and certificates

updated SMT2 certificates

added Z3 4.3.0 as component (for use with 'smt2' method)

updated SMT example certificates

added 'smt2_status' to keywords

avoid name clash

simplify index handling

more robust indices

correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs

move lemmas to theory file, towards textual proof reconstruction

simpler translation of 'div' and 'mod' for Z3

tuning

tuning

thread through step IDs from Z3 to Sledgehammer

adapted to ML structure renaming

tuning

avoid names that may clash with Z3's output (e.g. '')

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;