Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
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)
2011-06-06, by blanchet
tuning
2011-06-06, by blanchet
also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg
2011-06-06, by blanchet
reveal Skolems in new Metis
2011-06-06, by blanchet
don't throw exception on unknown constants (e.g. skolems), and give more precise type to applied functions
2011-06-06, by blanchet
slacker version of "fastype_of", in case a function has dummy type
2011-06-06, by blanchet
don't stumble on Skolem names
2011-06-06, by blanchet
conceal old Skolems in new Metis
2011-06-06, by blanchet
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
2011-06-06, by blanchet
use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is
2011-06-06, by blanchet
properly unmangle names in path finder
2011-06-06, by blanchet
only uncombine combinators in textual Isar proofs, not in Metis
2011-06-06, by blanchet
properly locate helpers whose constants have several entries in the helper table
2011-06-06, by blanchet
skip "hBOOL" in new Metis path finder
2011-06-06, by blanchet
don't pass "~ " to new Metis
2011-06-06, by blanchet
tuning
2011-06-06, by blanchet
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
2011-06-06, by blanchet
temporarily document "metisX"
2011-06-06, by blanchet
use "metisX" as fallback, since it's much faster than "metisFT"
2011-06-06, by blanchet
temporarily added "MetisX" as reconstructor and minimizer
2011-06-06, by blanchet
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
2011-06-06, by blanchet
show what failed to play
2011-06-06, by blanchet
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
2011-06-06, by blanchet
tuning
2011-06-06, by blanchet
killed odd connectives
2011-06-06, by blanchet
added Metis examples to test the new type encodings
2011-06-06, by blanchet
tuned CASC method
2011-06-06, by blanchet
clean up unnecessary machinery -- helpers work also with monomorphic type encodings
2011-06-06, by blanchet
added support for helpers in new Metis, so far only for polymorphic type encodings
2011-06-06, by blanchet
imported rest of new IMP
2011-06-06, by kleing
atLeastAtMostSuc_conv on int
2011-06-06, by kleing
fixed typo
2011-06-06, by kleing
updated SMT certificates
2011-06-05, by boehmes
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)
2011-06-05, by boehmes
changing the mira setting again for the mutabelle configuration
2011-06-03, by bulwahn
adding more settings to mira's mutabelle configuration
2011-06-03, by bulwahn
merged
2011-06-02, by nipkow
Added typed IMP
2011-06-02, by nipkow
adding quickcheck narrowing to mutabelle script; deactivating nitpick in mutabelle script momentarily because we are not monitoring the results effectively
2011-06-02, by bulwahn
adding invocation of exhaustive testing without using finite types to mutabelle
2011-06-02, by bulwahn
moving the distinction between invocation of testers and generators into test_goal_terms function in quickcheck for its usage with mutabelle
2011-06-02, by bulwahn
splitting Dlist theory in Dlist and Dlist_Cset
2011-06-02, by bulwahn
merged
2011-06-01, by nipkow
Made comments text
2011-06-01, by nipkow
Fixed denotational semantics
2011-06-01, by nipkow
Removed old IMP files
2011-06-01, by nipkow
Replacing old IMP with new Semantics material
2011-06-01, by nipkow
tuned lemmas
2011-06-01, by nipkow
fixed debilitating translation bug introduced in b6e61d22fa61 -- "equal" and "=" should always have arity 2
2011-06-01, by blanchet
setting up code generation for extended reals
2011-06-01, by bulwahn
new lemmas
2011-06-01, by nipkow
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
2011-06-01, by blanchet
more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
2011-06-01, by blanchet
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
2011-06-01, by blanchet
fixed Isabelle version of lightweight tag theorem, using "Thm.trivial" not "Thm.assume"
2011-06-01, by blanchet
ensured monomorphized facts have normalized zero var indexes, so that "find_var" doesn't fail later on
2011-06-01, by blanchet
fixed interaction between type tags and hAPP in reconstruction code
2011-06-01, by blanchet
implemented missing hAPP and ti cases of new path finder
2011-06-01, by blanchet
support lightweight tags in new Metis
2011-06-01, by blanchet
tuned names
2011-06-01, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip