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)