remove problematic Isar proof

added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around

robustly detect how many type args were passed to the ATP, even if some of them were omitted

make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types

drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation

tuning

fixed conjecture resolution bug for Vampire 1.0's TSTP output

ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded

Metis doesn't find an old proof in acceptable time now that higher-order equality reasoning is supported -- tuned proof script to help it

drop support for Vampire's native output format -- it has too many undocumented oddities, e.g. "BDD definition:" lines

use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.

further lower penalty associated with existentials in Sledgehammer's relevance filter, so that "exhaust" facts are picked up

reenabled equality proxy in Metis for higher-order reasoning

added "SMT." qualifier for constant to make it possible to reload "smt_monomorph.ML" from outside the "SMT" theory (for experiments) -- this is also consistent with the other SMT constants mentioned in this source file

reflect option renaming in doc + do not document the type systems poly_preds? and poly_tags?, since they are virtually identical to the non-? versions

unfold set constants in Sledgehammer/ATP as well if Metis does it too

do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings

renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly

added unfold set constant functionality to Meson/Metis -- disabled by default for now

remove unused parameter

reduced penalty associated with existential quantifiers

ensure that Auto Sledgehammer is run with full type information

fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized

don't give weights to built-in symbols

more robust exception handling in Metis (also works if there are several subgoals)

no penality for constants that appear in chained facts

gracefully declare fTrue and fFalse proxies' types if the constants only appear in the helpers

improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types

tune whitespace

added configuration options for experimental features

ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)

avoid "Empty" exception by making sure that a certain optimization only is attempted when it makes sense

added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options

added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option

allow each slice to have its own type system

renamed type systems for more consistency

updated versions;

added toplevel isabelle package -- reduce warnings with scala-2.9.0.final;

tuned;

minor adaption for scala-2.9.0.final;

proper configuration options Proof_Context.debug and Proof_Context.verbose; discontinued alias Proof.verbose = Proof_Context.verbose;

pretend that all versions of BSD are Linux, which might actually work due to binary compatibilty mode of these obsolete platforms;

more uniform naming of lemma

add a lemma about commutative append to List.thy

removed assumption from lemma List.take_add

no need for underscore.sty -- latex.ltx provides \textunderscore and \_ already;

removed \underscoreon which is from Larry's iman.sty, not underscore.sty;

further improved type system setup based on Judgment Days

allow each prover to specify its own formula kind for symbols occurring in the conjecture

better type system setup, based on Judgment Day

improving merge of code specifications by removing code equations of constructors after merging two theories

tuned;

tuned some syntax names;

tuned rail diagrams and layout;

merged;

tuning

reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems

added FIXME

no lies in debug output (e.g. "slice 2 of 1")

help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check

query typedefs as well for monotonicity

adding examples for invoking quickcheck with records

adding creation of exhaustive generators for records; simplifying dependencies in Main theory

hopefully this will help the SML/NJ type inference

reverted 6efda6167e5d because unsound -- Vampire found a counterexample

improve suggested type system list based on evaluation

I have an intuition that it's sound to omit the first type arg of an hAPP -- and this reduces the size of monomorphized problems quite a bit

removed unsound hAPP optimization

versions of ! and ? for the ASCII-challenged Mirabelle

smoother handling of ! and ? in type system names

tuning

compile + added monotonicity tests

documentation tuning

renamed "many_typed" to "simple" (as in simple types)

update type system documentation

added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)

document monotonic type systems

exploit inferred monotonicity

[mq]: nitpick_tuning

fixed cardinality computation for function types such as "'a -> unit"

monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.

proper case_names for int_cases, int_of_nat_induct; tuned some proofs, eliminating (cases, auto) anti-pattern;

added type annotation for SML/NJ

eta-expansion for SML/NJ

removed odd historical material;

merged

fixed per-ATP dangerous axiom detection -- embarrassing bugs introduced in change a7a30721767a

cosmetics

more conventional naming scheme: names_long, names_short, names_unique;

railsetup required for IsarRef/style;

fit page;

use existing \<hyphen>;

more precise syntax diagram;

simplified rail configuration;

provide \isabellestyle{itunderscore} (requires underscore.sty);

updated generated files;

proper treatment of empty name -- avoid excessive vertical space;

final \makeatother -- catcodes appear to be global;

fixed long name truncation logic

some documentation of @{rail} antiquotation;

more precise source position for @{rail};

sane paragraph layout;

updated configuration options -- no ML here;

tag ML as in IsarImplementation;

treat underscore as in IsarRef;

reactivated codegen example based on Lambda.thy;

formal Base theory;

reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"

whitespace tuning

make SML/NJ happiest

no need to generate fact numbers for polymorphic type systems -- this confuses the TPTP exporter

replaced some Unsynchronized.refs with Config.Ts

do not declare TPTP built-ins, e.g. $true

SNARK workaround

better default type systems for SNARK and ToFoF

tuning

recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)

generate tags for simps, intros, and elims in TPTP poblems on demand

proper default for TPTP source filed

have each ATP filter out dangerous facts for themselves, based on their type system