isabelle: Graph

removing unneccessary manual instantiations and dead definitions; hiding more constants and facts
2011-06-09, by bulwahn
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
2011-06-09, by bulwahn
adding narrowing engine for existentials
2011-06-09, by bulwahn
adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement
2011-06-09, by bulwahn
adding theory Quickcheck_Narrowing to HOL-Main image
2011-06-09, by bulwahn
adapting IsaMakefile
2011-06-09, by bulwahn
moving Quickcheck_Narrowing from Library to base directory
2011-06-09, by bulwahn
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
2011-06-09, by bulwahn
local simp rule in List_Cset
2011-06-09, by bulwahn
tuning
2011-06-09, by blanchet
compile
2011-06-09, by blanchet
cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)
2011-06-09, by blanchet
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)
2011-06-09, by blanchet
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
2011-06-09, by blanchet
removed needless function that duplicated standard functionality, with a little unnecessary twist
2011-06-09, by blanchet
removed more dead code
2011-06-09, by blanchet
be a bit more liberal with respect to the universal sort -- it sometimes help
2011-06-09, by blanchet
renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"
2011-06-09, by blanchet
merged
2011-06-08, by wenzelm
avoid duplicate facts, which confuse the minimizer output
2011-06-08, by blanchet
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
2011-06-08, by blanchet
restore comment about subtle issue
2011-06-08, by blanchet
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
2011-06-08, by blanchet
don't launch the automatic minimizer for zero facts
2011-06-08, by blanchet
don't generate unsound proof error for missing proofs
2011-06-08, by blanchet
renamed option to avoid talking about seconds, since this is now the default Isabelle unit
2011-06-08, by blanchet
fixed format selection logic for Waldmeister
2011-06-08, by blanchet
better default type system for Waldmeister, with fewer predicates (for types or type classes)
2011-06-08, by blanchet
simplified directory structure;
2011-06-08, by wenzelm
simplified directory structure;
2011-06-08, by wenzelm
further jedit build option;
2011-06-08, by wenzelm
build jedit as part of regular startup script (in that case depending on jedit_build component);
2011-06-08, by wenzelm
updated headers;
2011-06-08, by wenzelm
moved sources -- eliminated Netbeans artifact of jedit package directory;
2011-06-08, by wenzelm
removed obsolete Netbeans project setup;
2011-06-08, by wenzelm
support fresh build of jars;
2011-06-08, by wenzelm
more jvmpath wrapping for Cygwin;
2011-06-08, by wenzelm
more robust exception pattern General.Subscript;
2011-06-08, by wenzelm
pervasive Output operations;
2011-06-08, by wenzelm
modernized Proof_Context;
2011-06-08, by wenzelm
standardized header;
2011-06-08, by wenzelm
merged
2011-06-08, by boehmes
updated SMT certificates
2011-06-08, by boehmes
only collect substituions neither seen before nor derived in the same refinement step
2011-06-08, by boehmes
updated imports (cf. 93b1183e43e5);
2011-06-08, by wenzelm
merged
2011-06-08, by wenzelm
new Metis version
2011-06-08, by blanchet
removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
2011-06-08, by blanchet
exploit new semantics of "max_new_instances"
2011-06-08, by blanchet
minor optimization
2011-06-08, by blanchet
don't needlessly extensionalize
2011-06-08, by blanchet
don't needlessly presimplify -- makes ATP problem preparation much faster
2011-06-08, by blanchet
tuned
2011-06-08, by blanchet
removed experimental code submitted by mistake
2011-06-08, by blanchet
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
2011-06-08, by blanchet
removed removed option from documentation
2011-06-08, by blanchet
killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
2011-06-08, by blanchet
slightly faster/cleaner accumulation of polymorphic consts
2011-06-08, by blanchet
eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
2011-06-08, by krauss
more conventional variable naming
2011-06-08, by krauss
dropped outdated/speculative historical comments;
2011-06-08, by krauss
less redundant tags
2011-06-08, by krauss
removed generation of instantiated pattern set, which is never actually used
2011-06-08, by krauss
more precise type for obscure "prfx" field
2011-06-08, by krauss
clarified (and slightly modified) the semantics of max_new_instances
2011-06-07, by boehmes
use null_heap instead of %_. 0 to avoid printing problems
2011-06-07, by kleing
prioritize more relevant facts for monomorphization
2011-06-07, by blanchet
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
2011-06-07, by blanchet
workaround current "max_new_instances" semantics
2011-06-07, by blanchet
fixed missing proof handling
2011-06-07, by blanchet
optimized the relevance filter a little bit
2011-06-07, by blanchet
printing environment in mutabelle's log
2011-06-07, by bulwahn
merged
2011-06-07, by bulwahn
merged; manually merged IsaMakefile
2011-06-07, by bulwahn
splitting Cset into Cset and List_Cset
2011-06-07, by bulwahn
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
2011-06-07, by bulwahn
adding examples with existentials
2011-06-07, by bulwahn
renaming the formalisation of the birthday problem to a proper English name
2011-06-07, by bulwahn
adding compilation that allows existentials in Quickcheck_Narrowing
2011-06-07, by bulwahn
move away from old SMT monomorphizer
2011-06-07, by blanchet
tuning
2011-06-07, by blanchet
merged
2011-06-07, by blanchet
use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
2011-06-07, by blanchet
removed "verbose" option -- there won't be any verbosity in there, according to Sascha (yeah)
2011-06-07, by blanchet
nicely thread monomorphism verbosity in Metis and Sledgehammer
2011-06-07, by blanchet
clarified meaning of monomorphization configuration option by renaming it
2011-06-07, by boehmes
documentation tweaks
2011-06-07, by blanchet
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
2011-06-07, by blanchet
fixed typo in legacy feature message
2011-06-07, by blanchet
use new monomorphization code
2011-06-07, by blanchet
added (currently unused) verbose configuration option
2011-06-07, by blanchet
renamed ML function
2011-06-07, by blanchet
renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
2011-06-07, by blanchet
pass props not thms to ATP translator
2011-06-07, by blanchet
slighly more reasonable Vampire slices (until new monomorphizer is used)
2011-06-06, by blanchet
removed confusing slicing logic
2011-06-06, by blanchet
suggest first reconstructor that timed out, not last (i.e. metis not metisFT in most cases)
2011-06-06, by blanchet
effectively reenable slices for SPASS and Vampire -- they were disabled by mistake
2011-06-06, by blanchet
minor: curly brackets, not square brackets
2011-06-06, by blanchet
document metis better in Sledgehammer docs
2011-06-06, by blanchet
updated Sledgehammer message
2011-06-06, by blanchet
removed old optimization that isn't one anyone
2011-06-06, by blanchet
generate less type information in polymorphic case
2011-06-06, by blanchet
Metis code cleanup
2011-06-06, by blanchet
enable new Metis
2011-06-06, by blanchet
made "explicit_apply"'s smart mode (more) complete
2011-06-06, by blanchet
fall back in case path finder fails -- these errors are sometimes salvageable
2011-06-06, by blanchet
compile
2011-06-06, by blanchet
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"
2011-06-06, by blanchet
marked "metisF" as legacy -- nobody uses it or needs it
2011-06-06, by blanchet
more preparations towards hijacking Metis
2011-06-06, by blanchet
remove more occurrences of "metisX", preparing for the D Day when it will silently hijack "metis" and "metisFT"
2011-06-06, by blanchet
don't mention "metisX" so much in the docs -- it will go away soon
2011-06-06, by blanchet
reintroduced metisFT in example
2011-06-06, by blanchet
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
2011-06-06, by blanchet
imported patch metis_reconstr_give_type_infer_a_chance
2011-06-06, by blanchet
make "metisX"'s default more like old "metis"
2011-06-06, by blanchet
whitespace tuning
2011-06-06, by blanchet
tuned Metis examples
2011-06-06, by blanchet
more through tests of new Metis
2011-06-06, by blanchet
improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
2011-06-06, by blanchet
fixed type helper indices in new Metis
2011-06-06, by blanchet
improved ATP clausifier so it can deal with "x => (y <=> z)"
2011-06-06, by blanchet
avoid renumbering hypotheses
2011-06-06, by blanchet
fixed reconstruction of new Skolem constants in new Metis
2011-06-06, by blanchet
don't translate new Skolemizer assumptions in new Metis
2011-06-06, by blanchet
tuning
2011-06-06, by blanchet
fixed detection of Skolem constants in type construction detection code
2011-06-06, by blanchet