better parsing of options, in case the value has '='

show the relation

merged

renamed "sledgehammer_tactic.ML" to "sledgehammer_tactics.ML" (cf. module name); use it in "Mirabelle.thy"

added "sledgehammer_tac" as possible reconstructor in Mirabelle

merged

merged

also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)

Enabled non fully polymorphic map functions in subtyping

make SML/NJ and Poly/ML agree on the type of "before";

only depend on exisiting statements

merged

evaluator separating static and dynamic operations

tuned naming

evaluator separating static and dynamic operations

canonical handling of theory context argument

merged

evaluator separating static and dynamic operations

program is separate argument to serializer

more explicit structure for serializer invocation

merged

tuned proof

HOLogic.mk_id

avoid weird symbols in path

mechanism to keep SMT input and output files around in Mirabelle

proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them; removed "is_builtin_ext", which is too limited an API to be useful in light of the aforementioned restriction

added "smt_triggers" option to experiment with triggers in Sledgehammer; renamings (for consistency)

enable E weight generation with unofficial latest version of E (tentatively called E 1.2B) -- backed by Judgment Day

Cygwin: Poly/ML 5.4.0 requires libgmp3;

updated to polyml-5.4.0;

tuned;

updated for Poly/ML 5.4.0;

merged

avoid ML structure aliases (especially single-letter abbreviations)

added an additional beta reduction: unfolding of special quantifiers might leave terms unnormalized wrt to beta reductions

merged

configure domain package to work with HOL option type

make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction

simplify proofs

beta-reduction simproc uses lemma Abs_cfun_inverse2 instead of beta_cfun, to be more robust against eta-contraction

configure domain package to work with HOL sum type

replace list_map function with an abbreviation

merged

run SPASS and Vampire in SOS mode only if >= 50 facts are passed -- otherwise we are probably minimizing and then it's better if the prover is run only once with a full strategy

disable feature that was enabled by mistake

make exceptions more transparent in "debug" mode

remove spurious line

use the options provided by Stephan Schulz -- much better

optionally supply constant weights to E -- turned off by default until properly parameterized

merged

type_lifting for predicates

proper identifiers for consts and types;

some attempts to fit diagnostic output into regular TTY (75-80 characters per line);

tuned/clarified some component settings; explicit comments about common mistakes;

slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version); more robust rm_tree -- somewhat dangerous and not exported; tuned;

purged some comments (Locale_Test is already clean thanks to configuration options);

actually enable show_hyps option, unlike local_setup in 6da953d30f48 which merely affects the (temporary) auxiliary context;

merged

updated SMT certificates

re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)

derived SMT solver classes override inherited properties (properties of derived classes have a higher priority than properties of base classes)

perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required

merge

more convenient order of type variables

rename function cprod_map to prod_map

switch to transparent ascription, to avoid warning messages

types -> type_synonym

fix typo

merged

use deflations over type 'udom u' to represent predomains; removed now-unnecessary class liftdomain;

add lemma u_map_oo

replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings

minimize imports; move domain class instances for powerdomain types into Powerdomains.thy

powerdomain theories require class 'bifinite' instead of 'domain'

type 'defl' takes a type parameter again (cf. b525988432e9)

reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)

renamed Bifinite.thy to Representable.thy

renamed CompactBasis.thy to Compact_Basis.thy

merged

updated SMT certificates

removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions); removed odd retyping during folify (instead, keep all terms well-typed)

only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general); hide internal constants z3div and z3mod; rewrite div/mod to z3div/z3mod instead of adding extra rules characterizing div/mod in terms of z3div/z3mod

escape backticks in altstrings

added a timestamp to Nitpick in verbose mode for debugging purposes; turn on verbose mode for the examples

reduce the minimizer slack and add verbose information

two layers of timeouts seem to be less reliable than a single layer

move relevance filter into hard timeout

handle timeouts in Mirabelle more gracefully

made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever); disabled inductions (E and SPASS don't like them), but kept "ext" (seems more harmless)

Add mixins to locale dependencies.

Enable show_hyps, which appears to be set in batch mode but in an interactive session.

Add mixins to sublocale command.

tuning

higher hard timeout

lower threshold where the binary algorithm kick in and use the same value for automatic minimization

compile