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