merged

merge

reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving

merged

merged

(infixl "<<" 55) -> (infix "<<" 50)

simplify some proofs

remove unnecessary stuff from Discrete.thy

remove some unnecessary lemmas; move monofun_LAM to Cfun.thy

add lemma eq_imp_below

discontinue a bunch of legacy theorem names

move a few admissibility lemmas into FOCUS/Stream_adm.thy

simplify some proofs

compile -- 7550b2cba1cb broke the build

merge

recognize Vampire error

return the process return code along with the process outputs

better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)

merged

corrected slip: must keep constant map, not type map; tuned code

constructors to datatypes in code_reflect can be globbed; dropped unused code

adding code and theory for smallvalue generators, but do not setup the interpretation yet

make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice

better detection of completely irrelevant facts

always use a hard timeout in Mirabelle

use "smt" (rather than "metis") to reconstruct SMT proofs

don't pass too many facts on the first iteration of the SMT solver

catch TimeOut exception

ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns

if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed

removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway

make Nitpick datatype tests faster to make timeout less likely

invoke SMT solver in a loop, with fewer and fewer facts, in case of error

always honor the max relevant constraint

more robust treatment of suppressed quotes concerning replacement text -- for improved copy/paste behaviour;

updated generated files;

tweaked pdf setup to allow modification of \pdfminorversion;

merged;

updated generated files;

basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;

updated generated file;

more literal appearance of antiqopen/antiqclose;

'example_proof' is treated as non-schematic statement with irrelevant proof (NB: even regular proofs can contain unreachable parts wrt. the graph of proof promises);

continue after failed commands;

added Keyword.is_heading (cf. Scala version); tuned;

updated keywords;

mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;

somewhat more uniform timing markup in ML vs. Scala;

somewhat more uniform timing in ML vs. Scala;

added Markup.Double, Markup.Double_Property; tuned;

explicit "timing" status for toplevel transactions;

tuned;

tuned comments;

abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical

moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;

updated keywords;