merged

more precise characterization of built-in constants "number_of", "0", and "1"

merged

merged

adhere established Collect/mem convention more closely

merged

replaced misleading Fset/fset name -- these do not stand for finite sets

renamed slightly ambivalent crel to effect

disable triviality checking -- it might be the source of the spurious Interrupt exceptions that make it almost impossible to run Judgement Day

more precise error handling for Z3; refactored some of the error handling code shared by ATP and SMT

use "Thm.transfer" in Sledgehammer to prevent theory merger issues in "SMT_Solver.smt_filter" later on

make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT

try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates

added "verbose" option to Metis to shut up its warnings if necessary

added support for quantifier weight annotations

share and use more utility functions; slightly reduced complexity for Z3 proof rule 'rewrite'

added prove reconstruction for injective functions; added SMT_Utils to collect frequently used functions

generous timeout gives more breath in parallel run on less luxury machines

adding setup for exhaustive testing in example file

hiding enum

adapting example in Predicate_Compile_Examples

hiding the constants

improving function is_iterable in quickcheck

adding temporary options to the quickcheck examples

adapting the quickcheck examples

adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle

adding code equations for EX1 on finite types

adding code equation for function equality; adding some instantiations for the finite types

adding Enum to HOL-Main image and removing it from HOL-Library

moving Enum theory from HOL/Library to HOL

splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck

adding prototype for finite_type instantiations

adding option finite_types to quickcheck

adding test cases for smallcheck and adding examples where exhaustive testing is more successful

changed old-style quickcheck configurations to new Config.T configurations

adding temporary function test_test_small to Quickcheck

added useful function map_context_result to signature

moving the error handling to the right scope in smallvalue_generators

removing clone from function package and using the clean interface from Function_Relation instead

adding function generation to SmallCheck; activating exhaustive search space testing

adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict

generalized ensure_random_datatype to ensure_sort_datatype

renaming quickcheck generator code to random

ported sledgehammer_tactic to current development version

adding dependencies to IsaMakefile; adding sledgehammer_tactic in Mirabelle_Test

adding files to use sledgehammer as a tactic for non-interactive use

adding birthday paradoxon from some abandoned drawer

adding extensional function spaces to the FuncSet library theory

tuned

tuned

updated explode vs. raw_explode;

renamed raw "explode" function to "raw_explode" to emphasize its meaning;

total Symbol.explode (cf. 1050315f6ee2);

do not export Thy_Load.required, to avoid confusion about the interface;

merged

declare adm_chfin [simp]

add lemma cont_fun; remove unused lemma monofun_app

accumulated NEWS updates for HOLCF

section -> subsection

add lemma adm_prod_case