only testing theory LSC_Examples when GHC is installed on the machine

increasing timeout of example for counterexample generation

adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC

adding lazysmallcheck example theory to HOL-ex session

adding serial instance of finite_4 in lazysmallcheck; changing code equations for implies

replacing strings in generated Code resolves the changing names of Typerep in lazysmallcheck prototype

changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent

adding an example theory for Lazysmallcheck prototype

adding Lazysmallcheck prototype to HOL-Library

adding files for prototype of lazysmallcheck

removing debug message in quickcheck's postprocessor

fixing postprocessing; adding a configuration to enable and disable pretty presentation of quickcheck's counterexample

renaming dest_plain_fun to dest_fun_upds and adding handling of undefined for postprocessing of quickcheck

improving term postprocessing for counterexample presentation in quickcheck

tuned

finished and tested Z3 proof reconstruction for injective functions; only treat variables as atomic, and especially abstract constants (Isabelle's interpretation of these constants is most likely not known to Z3 and thus irrelevant for the proof)

improved formula for specialization, to prevent needless specializations -- and removed dead code

perform no arity check in debug mode so that we get to see the Kodkod problem

spark_end now joins proofs of VCs before writing *.prv file.

clarified

produce helpful mira summary for more errors

eliminated prems;

eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;

tuned proofs -- eliminated prems;

merged

merged

don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on

simplified Thy_Info.check_file -- discontinued load path;

discontinued legacy load path;

re-interpret ProofGeneralPgip.changecwd as Thy_Load.set_master_path, presuming that this is close to the intended semantics;

modernized imports;

observe standard header format;

removed spurious 'unused_thms' (cf. 1a65b780bd56);

isatest cygwin-poly-e: new memory management of polyml-svn could be more stable;

merged

merged

- Made sure that sort_defs is aware of constants introduced by add_type_def - add_def now compares Isabelle types rather than SPARK types to ensure that type abbreviations are taken into account

mention new Nitpick options

simplify "need" option's syntax

renamed "preconstr" option "need"

finally remove upper_bound_finite_set

separate settings for afp test

added missing spaces in output

lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on

unfold definitions in "preconstrs" option

robust handling of types occurring in "eval" and "preconstr" options but not in the goal

make "preconstr" option more robust -- shouldn't throw exceptions

merged

merged

declare ext [intro]: Extensionality now available by default

merged

removed dependency on Dense_Linear_Order

adding function Quickcheck.test_terms to provide checking a batch of terms

adding a function to compile a batch of terms for quickcheck with one code generation invocation

improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)

made "fixed_is_special_eligible_arg" smarter w.r.t. pairs, and fixed previous unintended behavior because "andalso" ties more tightly than "orelse"

if "total_consts" is set, report cex's as quasi-genuine

document new "total_consts" option

added "total_consts" option

added a few lemmas by Andreas Lochbihler

Corrected HOLCF/FOCUS dependency

Added material by David Trachtenherz

corrected HOLCF dependency on Nat_Infinity

got rid of lemma upper_bound_finite_set

merged

Some cleaning up

updated generated files

fixed manual (rule no longer exists)

removed support for tail-recursion from function package (now implemented by partial_function)

reactivate time measurement (partly reverting c27b0b37041a); export pretty_theorem, to display both internal or external facts

generalize find_theorems filters to work on raw propositions, too

merged

added simp lemma nth_Cons_pos to List

Refactor find_theorems to provide a more general filter_facts method

removed dead code/unused exports/speculative generality

recdef -> fun(ction)

removed unused lemma

recdef -> fun(ction); tuned

eliminated clones of List.upto

fix non-exhaustive pattern match in find_theorems

merged

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(-)

merged

remove confusing message

eliminated remdps in favor of List.remdups

recdef -> fun

recdef -> fun

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

recdef -> fun; curried

strengthened polymul.induct

dropped stupid name

removed duplicate declarations

recdef -> function

tuned proofs -- eliminated prems;

merged

adjust example

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