remove more occurrences of "metisX", preparing for the D Day when it will silently hijack "metis" and "metisFT"

don't mention "metisX" so much in the docs -- it will go away soon

reintroduced metisFT in example

make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s

imported patch metis_reconstr_give_type_infer_a_chance

make "metisX"'s default more like old "metis"

whitespace tuning

tuned Metis examples

more through tests of new Metis

improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)

fixed type helper indices in new Metis

improved ATP clausifier so it can deal with "x => (y <=> z)"

avoid renumbering hypotheses

fixed reconstruction of new Skolem constants in new Metis

don't translate new Skolemizer assumptions in new Metis

tuning

fixed detection of Skolem constants in type construction detection code

make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)

tuning

also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg

reveal Skolems in new Metis

don't throw exception on unknown constants (e.g. skolems), and give more precise type to applied functions

slacker version of "fastype_of", in case a function has dummy type

don't stumble on Skolem names

conceal old Skolems in new Metis

don't merge "hAPP"s even in unsound heavy modes, because "hAPP" then sometimes gets declared with too strict arguments ("ind"), and we lose some proofs

use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is

properly unmangle names in path finder

only uncombine combinators in textual Isar proofs, not in Metis

properly locate helpers whose constants have several entries in the helper table

skip "hBOOL" in new Metis path finder

don't pass "~ " to new Metis

tuning

gracefully handle the case where a constant is partially or not instantiated at all, as may happen when reconstructing Metis proofs for polymorphic type encodings

temporarily document "metisX"

use "metisX" as fallback, since it's much faster than "metisFT"

temporarily added "MetisX" as reconstructor and minimizer

ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)

show what failed to play

refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow

tuning

killed odd connectives

added Metis examples to test the new type encodings

tuned CASC method

clean up unnecessary machinery -- helpers work also with monomorphic type encodings

added support for helpers in new Metis, so far only for polymorphic type encodings

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