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