updated keywords

introduced manual version of "Auto Solve" as "solve_direct"

make "sledgehammer_params" work on single-threaded platforms

tuning

handle timeouts (to prevent failure from other threads); removed needless functions; added "metis" to the mix

update keywords

some partial_function examples

added ML antiquotation @{assert};

updated keywords;

integrated partial_function into HOL-Plain

first version of partial_function package

Complete_Partial_Order.thy: complete partial orders over arbitrary chains, with fixpoint theorem

merged

splitting Hotel Key card example into specification and the two tests for counter example generation

adding generator quickcheck

restructuring values command and adding generator compilation

moving general functions from core_data to predicate_compile_aux

updating to new notation in commented examples

merged

use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum

remove legacy comp_dbind option from domain package

change fixrec parser to not accept theorem names with (unchecked) option

tuned

rename lemma surjective_pairing_Sprod2 to spair_sfst_ssnd

add lemma strict3

do proofs using Rep_Sprod_simps, Rep_Ssum_simps; remove unused lemmas

make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun

direct instantiation unit :: discrete_cpo

remove finite_po class

simplify proofs about flift; remove unneeded lemmas

simplify proof

minimize imports

add type annotation to avoid warning

simplify some proofs, convert to Isar style

rename lemma spair_lemma to spair_Sprod

pcpodef (open) 'a lift

remove intro! attribute from {sinl,sinr}_defined

simplify proofs of ssumE, sprodE

merged

renamed nat_number

nat_number -> eval_nat_numeral

some cleanup in Function_Lib

merged

compile

added SMT solver to Sledgehammer docs

more robust handling of "remote_" vs. non-"remote_" provers

generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)

replaced references with proper record that's threaded through

fixed signature of "is_smt_solver_installed"; renaming

renamed modules

renamed files

took out "smt"/"remote_smt" from default ATPs until they are properly implemented

remove more needless code ("run_smt_solvers"); tuning

got rid of duplicate functionality ("run_smt_solver_somehow"); added minimization command to SMT solver message

bring ATPs and SMT solvers more in line with each other

make Sledgehammer minimizer fully work with SMT

generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well

first step in adding support for an SMT backend to Sledgehammer

use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."

cosmetics