isabelle: Changelog

recdef -> fun(ction)

removed unused lemma

recdef -> fun(ction); tuned

eliminated clones of List.upto

fix non-exhaustive pattern match in find_theorems

add lemma KL_divergence_vimage, mutual_information_generic

add lemma RN_deriv_vimage

use measure_preserving in ..._vimage lemmas

log is borel measurable

add name continuous_isCont to unnamed lemma

add example for case_product usage

setup case_product attribute in HOL and FOL

introduce attribute case_prod for combining case rules * * * [PATCH 1/9] Make tac independent of consumes From 1a53ef4c070f924ff8e69529b0c1b13fa2844722 Mon Sep 17 00:00:00 2001 --- case_product.ML | 11 ++++++----- 1 files changed, 6 insertions(+), 5 deletions(-) * * * [PATCH 2/9] Replace MRS by OF From da55d08ae287bfdc18dec554067b45a3e298c243 Mon Sep 17 00:00:00 2001 --- case_product.ML | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) * * * [PATCH 3/9] Clean up tactic From d26d50caaa3526c8c0625d7395467c6914f1a8d9 Mon Sep 17 00:00:00 2001 --- case_product.ML | 13 +++++-------- 1 files changed, 5 insertions(+), 8 deletions(-) * * * [PATCH 4/9] Move out get_consumes a bit more From 6ed5415f29cc43cea30c216edb1e74ec6c0f6c33 Mon Sep 17 00:00:00 2001 --- case_product.ML | 4 +++- 1 files changed, 3 insertions(+), 1 deletions(-) * * * [PATCH 5/9] Clean up tactic From d301cfe6377e9f7db74b190fb085e0e66eeadfb5 Mon Sep 17 00:00:00 2001 --- case_product.ML | 3 +-- 1 files changed, 1 insertions(+), 2 deletions(-) * * * [PATCH 6/9] Cleanup build_concl_prems From c30889e131e74a92caac5b1e6d3d816890406ca7 Mon Sep 17 00:00:00 2001 --- case_product.ML | 18 ++++++++---------- 1 files changed, 8 insertions(+), 10 deletions(-) * * * [PATCH 7/9] Split logic & annotation a bit From e065606118308c96e013fad72ab9ad89b5a4b945 Mon Sep 17 00:00:00 2001 --- case_product.ML | 26 ++++++++++++++++++-------- 1 files changed, 18 insertions(+), 8 deletions(-) * * * [PATCH 8/9] Remove dependency on consumes attribute From e2a4de044481586d6127bbabd0ef48d0e3ab57c0 Mon Sep 17 00:00:00 2001 --- case_product.ML | 46 ++++++++++++++++++++++------------------------ 1 files changed, 22 insertions(+), 24 deletions(-) * * * [PATCH 9/9] whitespace From 59f5036bd8f825da4a362970292a34ec06c0f1a2 Mon Sep 17 00:00:00 2001 --- case_product.ML | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-)

remove confusing message

eliminated remdps in favor of List.remdups

updated generated file;

scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;

modernized specifications;

dropped obsolete FIXMEs

merged, resolving spurious conflicts and giving up Reflected_Multivariate_Polynomial.thy from ab5d2d81f9fb;

eliminated global prems

modernized specification; curried

recdef -> fun; curried

strengthened polymul.induct

removed duplicate declarations

tuned proofs -- eliminated prems;

document new "preconstr" option

more work on "fix_datatype_vals" optimization (renamed "preconstruct")

more work on "fix_datatype_vals"

first steps in implementing "fix_datatype_vals" optimization

better fudge factors for CVC3 and Yices based on Judgment Day

exit code 127 can mean many things -- not just (and probably not) Perl missing

modernized specifications;

rename Nitpick's (internal) auxiliary lemmas

updated docs w.r.t. "nitpick_unfold" attribute

improve optimization

tweaked Nitpick based on C++ memory model example

renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics

always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"

give more weight to Frees than to Consts in relevance filter

don't distinguish between "fixes" and other free variables -- this confuses users

added a timeout around SMT preprocessing (notably monomorphization)

comments to find fudge factors easily

added test cases with quantifier occurring in first-order term positions

wrap occurrences of quantifiers in first-order terms (i.e., outside first-order formulas) in If-expressions

added is_IAbs; tuned brackets and comments

more idiomatic printing of let cascades and type variable constraints

modernized specifications;

more precise headers;

less verbose tracing;

standardized headers;

modernized specifications;

gracious timeout in "blocking" mode

make Nitpick's timeout mechanism somewhat more reliable/friendly; avoid producing warnings when invoked in "auto" mode

better fudge factors for Sledgehammer

adjust fudge factors

extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs

export more functionality of Sledgehammer to applications (for experiments)

export useful function (needed in a Sledgehammer-related experiment)

make experimental "Z3 ATP" work on Linux as well

adjusted fudge factors (based on Judgment Day runs)

generalized termination lemmas

strengthened induction rule; clarified some proofs

limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops); updated SMT certificate

more explicit errors to inform users about problems related to SMT solvers; fall back to remote SMT solver (if local version does not exist); extend the Z3 proof parser to accommodate for slight changes introduced by Z3 2.18

more explicit exit due to failed etc/settings -- normally return code 0=true and 1=false could be tolerated, but bash syntax errors also return 1;

eliminated somewhat obsolete warning -- former "$HOME/Isabelle" vs. "$HOME/isabelle" no longer exist;

more pretty set comprehension sugar

adjusting HOL-Mutabelle to changes in quickcheck

quickcheck can be invoked with its internal timelimit or without

quickcheck invokes TimeLimit.timeLimit only in one separate function

added option to Mirabelle Sledgehammer

reverted cs. 0a3fa8fbcdc5 -- motivation is unreconstructable, produces confusion in user space

fix handling of "fequal" in generated ATP problems -- the bug was visible if "explicit_apply" was on and "singleton_conv" is one of the facts being translated, as it resulted in an arity error in the ATP (e.g., E)

fix path to etc/settings and etc/components in doc

run all provers in blocking mode, even if a proof was already found -- this behavior is less confusing to the user

remove pointless clutter

make minimizer verbose

automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)

added "Z3 as an ATP" support to Sledgehammer locally

remove Z3 wrapper script, which is no longer necessary now that the SMT module generates SMT-LIB compliant files

added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation

tuned scope of Multithreading.interrupted vs. Multithreading.with_attributes;

changing auto-quickcheck to be considered a non-interactive invocation of quickcheck

discontinued obsolete lib/scripts/polyml-platform;

clarified comment -- ancienct PG 3.7.x is still in use;

discontinued obsolete alias HOL.thy for @{theory HOL} in ML;

prefer polyml-5.2.1 over odd polyml-5.3.0-old;

some shuffling of isatest settings, to ensure coverage of polyml-5.2.1, polyml-5.3.0, polyml-5.4.0, polyml-5.4.1 (SVN), smlnj/110.72;

reverted slightly odd eb5900951702: isatest-doc should work again due to 4b08499b3db1 (polyml-5.3.0 supports proper TimeLimit, as required for HOL-Nitpick-Examples);

available_provers ~> supported_provers (for clarity)

added support for bleeding-edge E weighting function "SymOffsetsWeight"

transformed lie into truth

enable SMT weights and triggers, since they lead to slight improvements according to the Judgment Day suite

improving sum type and option type term constructions for correct presentation in Smallcheck

Explicitly build HOLCF and ZF images. They are not part of the release any more.

added termination lemmas