local gensym based on Name.variant; do not export internals by default;

uniform use of flexflex_rule;

tuned name (cf. blast_stats);

more official options blast_trace, blast_stats;

merged

merged

resolving an issue with class instances that are pseudo functions in the OCaml code serializer

merged

fixed document generation for HOL

lemma: independence is equal to mutual information = 0

jensens inequality

lemmas about right derivative and limits

lemma about differences of convex functions

lemmas relating ln x and x - 1

use divide instead of inverse for the derivative of ln

adding ISABELLE_GHC environment setting to mira configuration isabelle makeall all on lxbroy10

renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;

document depth arguments of method "auto";

clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b); uniform handling of exceptions in depth_tac and blast_tac, discontinued separate blast_depth_tac; tuned blast_tac: atomize prems only once, outside DEEPEN;

clarified special incr_type_indexes;

tuned signature: Name.invent and Name.invent_names;

modernized structure ProofContext;

even more robust \isaspacing;

simplified Name.variant -- discontinued builtin fold_map;

some attempts at robust \isaspacing so that \isa{...} can be used in section headings etc. (need to avoid `\? for some reason);

discontinued Name.variant to emphasize that this is old-style / indirect;

prefer new-style Name.invents;

more tight name invention -- avoiding old functions;

\frenchspacing for formal isabelle style avoids extra space in situations like ``@{text "?"}'' followed by plain text;

tuned;

NEWS

correcting import theory of examples

fixing code generation test

removing char setup

removing unneccessary manual instantiations and dead definitions; hiding more constants and facts

adding a nicer error message for quickcheck_narrowing; hiding fact empty_def

adding narrowing engine for existentials

adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement

adding theory Quickcheck_Narrowing to HOL-Main image

adapting IsaMakefile

moving Quickcheck_Narrowing from Library to base directory

compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators

local simp rule in List_Cset

tuning

compile

cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)

added a really fully typed translation as a fallback for Metis, in rare cases where Metis correctly proves a theorem but has type-unsound steps in it (which is likelier to happen with some of the lighter translations)

improve sort inference in Metis proofs -- in some rare cases Metis steals Isabelle's variable names and the sorts must then be inferred as well

removed needless function that duplicated standard functionality, with a little unnecessary twist

removed more dead code

be a bit more liberal with respect to the universal sort -- it sometimes help

renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"

merged

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

move away from old SMT monomorphizer

tuning

merged

use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing

removed "verbose" option -- there won't be any verbosity in there, according to Sascha (yeah)

nicely thread monomorphism verbosity in Metis and Sledgehammer

clarified meaning of monomorphization configuration option by renaming it

documentation tweaks

obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be

fixed typo in legacy feature message

use new monomorphization code

added (currently unused) verbose configuration option

renamed ML function

renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules

pass props not thms to ATP translator

slighly more reasonable Vampire slices (until new monomorphizer is used)

removed confusing slicing logic

suggest first reconstructor that timed out, not last (i.e. metis not metisFT in most cases)

effectively reenable slices for SPASS and Vampire -- they were disabled by mistake

minor: curly brackets, not square brackets

document metis better in Sledgehammer docs

updated Sledgehammer message

removed old optimization that isn't one anyone

generate less type information in polymorphic case

Metis code cleanup

enable new Metis

made "explicit_apply"'s smart mode (more) complete

fall back in case path finder fails -- these errors are sometimes salvageable

compile

change var name as a workaround for rare issue in Metis's reconstruction code -- namely, "find_var" fails because "X = X" is wrongly mirrorred as "A = A"

marked "metisF" as legacy -- nobody uses it or needs it

more preparations towards hijacking Metis

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)