change license, with Joe Hurd's permission

new version of the Metis files

remove old sources

remove "atoms" from the list of options with default values

remove unreferenced identifiers

make Auto Nitpick go through fewer scopes

move equation up where it's not ignored

correctly thread parameter through

indicate triviality in the list of proved things

indicate which goals are trivial

tuning

tuning

keep track of trivial vs. nontrivial calls using "try" for 30 seconds

change signature of "Try.invoke_try" to make it more flexible

use 30 s instead of 60 s as the default Sledgehammer timeout; very few proofs are lost this way (esp. thanks to the parallel use of provers, cf. Boehme & Nipkow 2010), and this is much more tolerable for users

no timeout for Auto Try, since the Auto Tools framework takes care of timeouts

add Proof General option

make Try's output more concise

added Auto Try to the mix of automatic tools

crank up Auto Tools timeout; instead of 2500 ms (for Auto Solve) + 2500 ms (for Auto Quickcheck/Nitpick), have 4000 ms as the cumulative timeout

make Auto Solve part of the "Auto Tools"

tuning

tuning

tuning

tuning

finished renaming "Auto_Counterexample" to "Auto_Tools"

start renaming "Auto_Counterexample" to "Auto_Tools"; Auto Sledgehammer now uses so the name is clearly wrong

setup Auto Sledgehammer

make Mirabelle happy

added Auto Sledgehammer docs

change order of default ATPs; put SPASS first so that it's picked up by Auto Sledgehammer

implemented Auto Sledgehammer

document changes to Auto Nitpick

change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)

always handle type variables in typedefs as global

removed duplicate lemma

adding two more examples to example theory

handling function types more carefully than in e98a06145530

adding order on modes

removing obsolete argument in prepare_intrs; passing context instead of theory in prepare_intrs

type antiquotation: allow arbitrary type abbreviations, but fail with user-space exception on bad input

merged

added Imperative HOL overview

print mode for Imperative HOL overview; tuned and more accurate dependencies

'class' and 'type' are now antiquoations by default

merged

merged

renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI

added and renamed lemmas

merged

directly computing the values of interest instead of composing functions in an unintelligent way that causes exponential much garbage; using the latest theory

added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet

use eta-contracted version for occurrence check (avoids possible non-termination) Test case: lemma "fwrap f = (%v. f v) ==> P f" apply clarify; pointed out by Thomas Sewell

tuned signature; tuned comments;

Type_Infer.finish: index 0 -- freshness supposedly via Name.invents; Type_Infer.fixate_params: full Proof.context;

simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;

tuned;

Type_Infer.preterm: eliminated separate Constraint;

Type_Infer.infer_types: plain error instead of kernel exception TYPE;

load type_infer.ML later -- proper context for Type_Infer.infer_types; renamed Type_Infer.polymorphicT to Type.mark_polymorphic;

common Type.appl_error, which also covers explicit constraints;

eliminated aliases of Type.constraint;

tuned;

tuned messages; tuned comments;

avoid extra wrapping for interrupts;

tuned markup;

updated keywords;

proper antiquotations;

fixed antiquotation;

updated generated file;

updated config options;

removed spurious addition from 9e58f0499f57;

merged

improved error message for common mistake (fun f where "g x = ...")

adding another String.literal example

fiddling with the correct setup for String.literal

refactoring mode inference so that the theory is not changed in the mode inference procedure

Haskell == is infix, not infixl

more correct dependencies

merged

use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson

use the Meson cutoff as the cutoff for using definitional CNF -- it's simpler that way

clarify comment

improve on 65903ec4e8e8: fix more "add_ffpair" exceptions in failed ATP proofs

allow Sledgehammer proofs containing nameless local facts with schematic variables in them

tuning

more precise error messages when Vampire is interrupted or SPASS runs into an internal bug

better error reporting when the Sledgehammer minimizer is interrupted

add cutoff beyond which facts are handled using definitional CNF

"resurrected" a Metis proof

replace two slow "metis" proofs with faster proofs

workaround to avoid subtle "add_ffpairs" unification exception in Sledgehammer; to reproduce the old bug, replace the command by(rule new_Addr_SomeD) on line 27 of Jinja/J/TypeSafe.thy with by (metis new_Addr_SomeD)

improve SInE-E failure message

merged

adding an example with integers and String.literals

adding an example to show how code_pred must be invoked with locales

removing report from the arguments of the quickcheck functions and refering to it by picking it from the context

changing the container for the quickcheck options to a generic data

Tidied up proofs using sledgehammer, also deleting unnecessary semicolons

changing String.literal to a type instead of a datatype

increasing the number of iterations to ensure to find a counterexample by random generation

only conceal primitive definition theorems, not predicate names

merged

modernized primrec

Markup_Tree is already scalable;

Isabelle_Markup.tooltip: explicit indication of ML;

Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);

primitive use_text: let interrupts pass unhindered;

Isabelle.load_icon with some sanity checks;

ML_Compiler.eval: reported positions need to contain offset, to avoid displaced reports due to synthesized line numbers;

NEWS: some notes on interrupts;

refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;

removed dead code;

avoid handling interrupts in user code;

Meson.make_clauses_unsorted: removed spurious debug code stemming from 5146d640aa4a -- must not handle arbitrary exceptions in user space;

main command loops are supposed to be uninterruptible -- no special treatment here;

Exn.is_interrupt: include interrupts that have passed through the IO layer;

more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;

avoid mixing of static and runtime errors in compiler output, to accomodate Proof General; refrain from absorbing Exn.Interrupt, to accomodate asynchronous interaction; actually observe Isabelle/ML naming conventions in exception STATIC_ERRORS;

ML_Compiler.eval: discontinued extra "Static Errors" of raw Poly/ML;