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;

reflect actual content of /home/isabelle/.html-data/cgi-bin/hgwebdir.cgi;

eliminated spurious "firstline" filters for improved display of Isabelle history logs: one item per line, without special headline; more uniform shortlogentry and filelogentry;

reflect actual content of /home/isabelle-repository/hgweb-templates/isabelle by krauss;

obsolete -- python installation on www4 is not modified (despite remaining "firstline" in graph and syndication views);

explicit indication of some remaining violations of the Isabelle/ML interrupt model;

updated generated file, overwriting 55a1693affb6 whose content appears to be in the thy source already;

proper spelling; proper format;

merged

Extend convex analysis by Bogdan Grechuk

merged

fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)

make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information

pass proper type to SMT_Builtin.is_builtin

remove " s" suffix since seconds are now implicit

ignore facts with only theory constants in them

cosmetics

use the SMT integration's official list of built-ins

added class relation group_add < cancel_semigroup_add

merged

changing timeout to real value; handling Interrupt and Timeout more like nitpick does

added two lemmas about injectivity of concat to the list theory

adding documentation of some quickcheck options

merged

Code.check_const etc.: reject too specific types

corrected quoting

added lemma length_alloc

dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document

added note on countable types

simulate more closely the behaviour of the tactic

merged

merged

merged

dropped debug message

more precise text

SMLdummy target

fixed typos

moved theory Quicksort from Library/ to ex/

Theory Multiset provides stable quicksort implementation of sort_key.

added code lemmas for stable parametrized quicksort

tuned proof

moved file in makefile to reflect actual dependencies

give E one more second, to prevent cases where it finds a proof but has no time to print it

use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages; updated docs

don't be overly verbose in Sledgehammer's minimizer

standardize on seconds for Nitpick and Sledgehammer timeouts

cleaned up

added property "tooltip-margin";

clarified tooltips: message output by default, extra info via control/command;

warn in correlation with report -- avoid spurious message duplicates;

tuned;

feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);

merged

updated SMT certificates

standardize timeout value based on reals

merged

merged

change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'

merged

renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun

renamed lemma cont2cont_Rep_CFun to cont2cont_APP

simplify proof of typedef_cont_Abs

rename constant trifte to tr_case

add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'

make syntax of continuous if-then-else consistent with HOL if-then-else

rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff

polyml_as_definition does not require explicit dependencies on external ML files

explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;

discontinued obsolete function sys_error and exception SYS_ERROR;

replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;

replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;