Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.

Replace surj by abbreviation; remove surj_on.

adjust Sledgehammer/SMT fudge factor

clarified Par_List.managed_results, with explicit propagation of outermost physical interrupt to forked futures (e.g. to make timeout apply here as expected and prevent zombies);

merge

cosmetics

eta-reduce on the fly to prevent an exception

merged

Added the simplest finite Ramsey theorem

reverted c059d550afec -- the triviality check had apparently nothing to do with spontaneous Interrupt exceptions

set Metis option on correct context, lest it be ignored

make "debug" mode of Sledgehammer/SMT more liberal

fix check for builtinness of 0 and 1 -- these aren't functions

added "no_atp" for fact that confuses the SMT normalizer and that doesn't help ATPs anyway

document requirement on theory import

corrected abd4e7358847 where SOMEthing went utterly wrong

merged

swap names for built-in tester functions (to better reflect the intuition of what they do); eta-expand all built-in functions (even those which are only partially supported)

instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)

more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers

removing Enum.in_enum from the claset

merged

be more precise: only treat constant 'distinct' applied to an explicit list as built-in

be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)

announcing some latest change (d40b347d5b0b)

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

merged

First-order pattern matching: catch a rogue exception (differing numbers of arguments)

eval simp rules for predicate type, simplify primitive proofs

generalized type

made smlnj happy

merged

proper qualification needed due to shadowing on theory merge

more appropriate name for property

mapper for sum type

mapper for option type

mapper for list type; map_pair replaces prod_fun

map_pair replaces prod_fun

mapper for mulitset type

mapper for mapping type

mapper for fset type

mapper for dlist type

map_fun combinator in theory Fun

some updates after 2 years of Mercurial usage;

mention Sledgehammer with SMT

enabled SMT solver in Sledgehammer by default

merged

keep variables bound

remove "Time limit reached" as potential error, because this is sometimes generated for individual slices and not for the entire problem

merged

infer variances of user-given mapper operation; proper thm storing

code eqn for slice was missing; redefined splice with fun

move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain

merged

typedef (open) unit

add bind_bind rules for powerdomains

merged

emerging Isar command interface

fixed typo

updated keywords

ML signature interface