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

let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)

use minimizing prover in Mirabelle

renamed function to run prover with minimizer and changed signature to clarify its semantics and make it a drop in replacement for "get_prover"

factored out running a prover with (optionally) an implicit minimizer phrase

merged;

remove option that doesn't work in Mirabelle anyway (Mirabelle uses Sledgehammer_Provers, not Sledgehammer_Run)

more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle

convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented

merged

put the SMT weights back where they belong, so that they're also used by Mirabelle

added debugging option to find out how good the relevance filter was at identifying relevant facts

extra checking of name bindings for classes, types, consts; tuned;

more explicit references to structure Raw_Simplifier;

merged

merged

merged

Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature);

dropped slightly odd Conv.tap_thy

avoid slightly odd Conv.tap_thy

allocate intermediate directories in module hierarchy

export experimental options

merged

compile

run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers

make timeout part of the SMT filter's tail

merge

split "smt_filter" into head and tail

fewer facts to SInE-E

Z3 sometimes reports two errors, with the first one referring to line 1 for some strange reason -- but it makes no sense to kill line 1, so we traverse the errors in reverse and consider only the last error

trap one more Z3 error

fixed the command-line syntax for setting Yices' random seed

merged

updated SMT certificates

fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order; fixed introduction of explicit application: use explicit application for every additional argument (grouping of arguments caused confusion when translating into the intermediate format)

adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real

updated generated file;

replaced command 'nonterminals' by slightly modernized version 'nonterminal';

renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;

tuned signature;

clarified exports of structure Simplifier;

refer to regular structure Simplifier;

tuned;

updated SMT certificates

more precise/correct SMT error handling

fixed off-by-one and return proper error code -- never underestimate the number of oddities in Perl

discriminate SMT errors a bit better

keep track of errors in Z3 input file for debugging purposes

better propagation of stdout in case of failure + comply with strict/warnings

merge

cleaner handling of temporary files

merged

made sml/nj happy

added self-correcting wrapper for Z3 -- see comment in the file for details

impose a limit on the breadth of monomorphization (in addition to on the depth) to prevent an explosion of the number of monomorphic instances

no need to do a super-duper atomization if Metis fails afterwards anyway

removed unused variable

robustly handle SMT exceptions in Sledgehammer

make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive

reintroduce the higher penalty for skolems

tuning

comment tuning

get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts

fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)

make it more likely that induction rules are picked up by Sledgehammer

generalize the Vampire parser some more to cope with things like "{2, 3\}" seen in some proofs

add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already

instantiate induction rules automatically

merged

fix lambda-lifting: take level of bound variables into account and also apply bound variables from outer scope

fixed introduction of explicit application function: bound variables always need explicit application if they are applied to some term

fixed eta-expansion: introduce a couple of abstractions at once

merged

made sml/nj happy

removing file refute_isar.ML that was missed in 4006f5c3f421

added nitpick to mutabelle script

reactivating nitpick in Mutabelle

more appropriate closures for static evaluation