imported rest of new IMP

atLeastAtMostSuc_conv on int

fixed typo

updated SMT certificates

made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)

changing the mira setting again for the mutabelle configuration

adding more settings to mira's mutabelle configuration

merged

Added typed IMP

adding quickcheck narrowing to mutabelle script; deactivating nitpick in mutabelle script momentarily because we are not monitoring the results effectively

adding invocation of exhaustive testing without using finite types to mutabelle

moving the distinction between invocation of testers and generators into test_goal_terms function in quickcheck for its usage with mutabelle

splitting Dlist theory in Dlist and Dlist_Cset

merged

Made comments text

Fixed denotational semantics

Removed old IMP files

Replacing old IMP with new Semantics material

tuned lemmas

fixed debilitating translation bug introduced in b6e61d22fa61 -- "equal" and "=" should always have arity 2

setting up code generation for extended reals

new lemmas

handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes

more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done

make sure no warnings are given for polymorphic facts where we use a monomorphic instance

fixed Isabelle version of lightweight tag theorem, using "Thm.trivial" not "Thm.assume"

ensured monomorphized facts have normalized zero var indexes, so that "find_var" doesn't fail later on

fixed interaction between type tags and hAPP in reconstruction code

implemented missing hAPP and ti cases of new path finder

support lightweight tags in new Metis

tuned names

export one more function

clausify "<=>" (needed for some type information)

distinguish different kinds of typing informations in the fact name

splitting RBT theory into RBT and RBT_Mapping

creating a free variable with proper name and local mixfix syntax (cf. db9b9e46131c)

code preprocessor applies simplifier when schematic variables are fixed to free variables to allow rewriting with congruence rules in the preprocessing steps

make SML/NJ happier

make sure "Trueprop" is removed before combinators are added -- the code is fragile in that respect

speed up example by disabling preplay, and temporarily comment out a broken Sledgehammer call

updated SMT certificates

proper nesting of loops in new monomorphizer; less duplication of code in new monomorphizer; drop output of warnings of new monomorphizer

use new monomorphizer for SMT; simplify the monomorphizer by inlining functions and proper passing of arguments

merged

Quickcheck Narrowing only requires one compilation with GHC now

splitting test_goal_terms in Quickcheck into smaller basic functions

adding registration of testers in Quickcheck for its use in Quickcheck_Narrowing

compile

compile

monomorphize in the new Metis if the type system calls for it

use "monomorph.ML" in "ATP" theory (so the new Metis can use it)

fixed comment

fixed new path finder for type information tag

no need for type arguments with "xxx_tags_heavy" type system

use ":" for type information (looks good in Metis's output) and handle it in new path finder

tuned name

tuned name

make "prepare_atp_problem" more robust w.r.t. choice of type system

parse optional type system specification

tuning

proper handling of type variable classes in new Metis

fixed recursive call in new path finder and (untested:) handle hAPP

don't preprocess twice

more robust and simpler adjustment computation

more work on new Metis

tuning

more work on new metis that exploits the powerful new type encodings

tuning

removed obscure option

added "metisX" syntax (temporary)

compile

added new metis mode, with no implementation yet

tuning

first step in sharing more code between ATP and Metis translation

more precise authorship, reflecting my own ignorance and hg annotate

generate raw induction rule as instance of generic rule with careful treatment of currying

generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type

admissibility on option type

also manage induction rule; tuned data slot

improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms

merged

Workaround for bug involving makeindex, hyperref and the | symbol

parameterize print_theorems over actual search function

added experimental yxml_find_theorems web service (but no client yet)

generic ScgiServer.simple_handler

moved html templates to a separate module, making their awkward signatures explicit

attempt to clarify code; removed "handle _" and dead code

(de)serialization for search query and result

explicit type for search queries

moved questionable goal modification out of filter_theorems

exported raw query parser; removed inconsistent clone

separate query parsing from actual search

fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other

document new explicit apply

made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly

don't slice if there are too few facts

nicer failure message when one-line proof reconstruction fails

make SML/NJ happy

avoid monomorphic encoding with so many facts -- it makes the old monomorphizer explode on some examples

make all messages urgent in verbose mode

minimize automatically even if Metis failed, if the external prover was really fast

fixed syntax of min options

no more bonus for E -- with the soft timeout, this punishes everybody -- the bonus was designed for a hard timeout

better merging of similar outputs

update minimization documentation

imported patch sledge_doc_metis_as_prover

automatically minimize with Metis when this can be done within a few seconds

minimize with Metis if possible

support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing

Workaround for hyperref bug affecting index entries involving the | symbol

improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of

automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option

merged multiple heads

Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler

always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated

normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages

function tutorial: do not omit termination proof, even when discussing other things

added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization

document new "try"

tuned comments

new timeout section (cf. Nitpick manual)

cleanup proof text generation code

more Sledgehammer documentation updates

minor update

try both "metis" and (on failure) "metisFT" in replay

show time taken for reconstruction

unbreak "max_potential" logic

more concise output

compile

use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)

repaired theory merging and defined/used helpers

make Sledgehammer a little bit less verbose in "try"

handle non-auto try cases gracefully in Try Methods

handle non-auto try case gracefully in Solve Direct

prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators

update SML section of documentation

handle non-auto try case gracefully in Nitpick

handle non-auto try case of Sledgehammer better

added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods

removed FIXME: "try_methods" doesn't take a clasimpmod, because it needs to generate Isar proof text in case of success and hence needs total control over its arguments

renamed "Auto_Tools" "Try"

removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP

renamed "try" "try_methods"

renamed "metis_timeout" to "preplay_timeout" and continued implementation

minor fixes to Sledgehammer docs

shorten minimizer command further, exploiting until-now-undocumented syntax

minor tweaks to the Nitpick documentation

added syntax for specifying Metis timeout (currently used only by SMT solvers)

readded Waldmeister as default to the documentation and other minor changes

reintroduced Waldmeister but limit the number of remote threads created

renamed "minimize" to "min" to make Sledgehammer output a little bit more concise

minor doc adjustments

make output more concise

merge timeout messages from several ATPs into one message to avoid clutter

fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context

tuning

mention contributions from LCP and explain metis and metisFT encodings

fixed trivial fact detection

cleaner handling of equality and proxies (esp. for THF)

recognize more ATP failures

fully support all type system encodings in typed formats (TFF, THF)

take out Waldmeister from default for now -- success rate too low on Judgment Day

document relevance filter a bit more

always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)

towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)

instance inat for complete_lattice

iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)

integral strong monotone; finite subadditivity for measure

composition of convex and measurable function is measurable

introduce independence of two random variables

add lemma indep_distribution_eq_measure

add lemma indep_rv_finite

generalize setsum_cases

add lemma borel_0_1_law

add lemma sigma_sets_singleton

use abbrevitation events == sets M

add lemma kolmogorov_0_1_law

add lemma indep_sets_collect_sigma

improving code_int setup in Quickcheck_Narrowing; adding partial_term_of class in Quickcheck_Narrowing

extending terms of Code_Evaluation by Free to allow partial terms

adhoc event handler to insert 'sendback' text into the buffer, replacing the original command

css rules for highlighting sendback text

invert event propagation flag -- in lobobrowser api, true means re-propagate

eta-expand to make SML/NJ happy

ensure that the argument of logical negation is enclosed in parentheses in THF mode

hack to obtain potable step names from Waldmeister

respect user's intention better when setting the CNF_UEQ type system (esp. w.r.t. "erased")

further reduce the number of facts passed to less used remote ATPs

added quietness flag

pass fewer relevant facts to less used remote systems

more work on parsing LEO-II proofs and extracting uses of extensionality

tuning

more work on parsing LEO-II proofs without lambdas

slightly gracefuller handling of LEO-II and Satallax output

document primitive support for LEO-II and Satallax

identify HOL functions with THF functions

started adding support for THF output (but no lambdas)

eliminated more code duplication in Nitrox

reduce code duplication in Nitrox

use \<emdash> rather than \<midarrow>

fixed de Bruijn index bug

use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things

filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations

clearer SystemOnTPTP errors

give fewer equations to Waldmeister

detect inappropriate problems and crashes better in Waldmeister

tuning -- the "appropriate" terminology is inspired from TPTP

pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding

move lemmas to Extended_Reals and Extended_Real_Limits

separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform

reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive

fun command produces warning when patterns are incomplete (somewhat analogous to primrec)

added message when Waldmeister isn't run

slightly improved documentation

improved Waldmeister support -- even run it by default on unit equational goals

fish out axioms in Waldmeister output

removed SNARK hack now that SNARK is fixed

recognize one more SystemOnTPTP error

document Waldmeister

added support for remote Waldmeister

added Waldmeister

reorganized ATP formats a little bit

tuned;

removed odd remains of low-level session management;

moved incr_boundvars; discontinued low-level term operations;

modernized and re-unified Thm.transfer;

removed obsolete material (superseded by implementation manual);

removed somewhat low-level stuff (cf. attribute "swapped" in isar-ref);

updated and re-unified classical proof methods; tuned;

tuned;

updated and re-unified classical rule declarations;

moved/updated introduction to Classical Reasoner;

tuned secref (still dangling);

updated and re-unified material on simprocs;

removed some old stuff;

tuned headings;

some material on "Generalized elimination and cases";

some material on "Structured induction proofs";

some material on "Structured Natural Deduction"; tuned;

some material on "Calculational reasoning";

tuned;

added Synopsis, with some "Notepad" material;

more accurate deps;

turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex);

moved/updated basic HOL overview;

updated and re-unified (co)inductive definitions in HOL; modernized examples;

clarified current 'primrec' vs. old 'recdef'; updated examples from src/HOL/Induct;

record examples;

updated and simplified HOL datatype examples (NB: special treatment of distinctness has been discontinued in the vicinity of 542b34b178ec);

updated and re-unified HOL rep_datatype;

rearranged some sections;

updated and re-unified HOL typedef, with some live examples;

optional jedit_build/etc/user-settings enable to override defaults produced by late component initialization;

merged

add divide_.._cancel, inverse_.._iff

add surj_vimage_empty