avoid duplicate facts, which confuse the minimizer output

pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types

restore comment about subtle issue

made "query" type systes a bit more sound -- local facts, e.g. the negated conjecture, may make invalid the infinity check, e.g. if we are proving that there exists two values of an infinite type, we can use the negated conjecture that there is only one value to derive unsound proofs unless the type is properly encoded

don't launch the automatic minimizer for zero facts

don't generate unsound proof error for missing proofs

renamed option to avoid talking about seconds, since this is now the default Isabelle unit

fixed format selection logic for Waldmeister

better default type system for Waldmeister, with fewer predicates (for types or type classes)

simplified directory structure; recovered README.html;

simplified directory structure;

further jedit build option; misc tuning;

build jedit as part of regular startup script (in that case depending on jedit_build component); misc tuning and simplification;

updated headers;

moved sources -- eliminated Netbeans artifact of jedit package directory;

removed obsolete Netbeans project setup;

support fresh build of jars; prefer pushd/popd, to avoid unclarity about fail/exit within sub-shell;

more jvmpath wrapping for Cygwin;

more robust exception pattern General.Subscript;

pervasive Output operations;

modernized Proof_Context;

standardized header;

merged

updated SMT certificates

only collect substituions neither seen before nor derived in the same refinement step

updated imports (cf. 93b1183e43e5);

merged

new Metis version

removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"

exploit new semantics of "max_new_instances"

minor optimization

don't needlessly extensionalize

don't needlessly presimplify -- makes ATP problem preparation much faster

tuned

removed experimental code submitted by mistake

make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization

removed removed option from documentation

killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"

slightly faster/cleaner accumulation of polymorphic consts

eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions

more conventional variable naming

dropped outdated/speculative historical comments; adapted to isabelle commenting style; tuned

less redundant tags

removed generation of instantiated pattern set, which is never actually used

more precise type for obscure "prfx" field

clarified (and slightly modified) the semantics of max_new_instances

use null_heap instead of %_. 0 to avoid printing problems

prioritize more relevant facts for monomorphization

more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs

workaround current "max_new_instances" semantics

fixed missing proof handling

optimized the relevance filter a little bit

printing environment in mutabelle's log

merged

merged; manually merged IsaMakefile

splitting Cset into Cset and List_Cset

adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing

adding examples with existentials

renaming the formalisation of the birthday problem to a proper English name

adding compilation that allows existentials in Quickcheck_Narrowing