| Tue, 31 May 2011 11:16:52 +0200 |
krauss |
generate raw induction rule as instance of generic rule with careful treatment of currying
|
changeset |
files
|
| Tue, 31 May 2011 11:16:34 +0200 |
krauss |
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
|
changeset |
files
|
| Tue, 31 May 2011 11:11:17 +0200 |
krauss |
admissibility on option type
|
changeset |
files
|
| Mon, 23 May 2011 21:34:37 +0200 |
krauss |
also manage induction rule;
|
changeset |
files
|
| Mon, 30 May 2011 17:55:34 +0200 |
bulwahn |
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
|
changeset |
files
|
| Mon, 30 May 2011 16:15:37 +0100 |
paulson |
merged
|
changeset |
files
|
| Mon, 30 May 2011 16:10:12 +0100 |
paulson |
Workaround for bug involving makeindex, hyperref and the | symbol
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
parameterize print_theorems over actual search function
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
added experimental yxml_find_theorems web service (but no client yet)
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
generic ScgiServer.simple_handler
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
moved html templates to a separate module, making their awkward signatures explicit
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
attempt to clarify code; removed "handle _" and dead code
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
(de)serialization for search query and result
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
explicit type for search queries
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
moved questionable goal modification out of filter_theorems
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
exported raw query parser; removed inconsistent clone
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
separate query parsing from actual search
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
document new explicit apply
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
don't slice if there are too few facts
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
nicer failure message when one-line proof reconstruction fails
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
make SML/NJ happy
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
avoid monomorphic encoding with so many facts -- it makes the old monomorphizer explode on some examples
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
make all messages urgent in verbose mode
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
minimize automatically even if Metis failed, if the external prover was really fast
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
fixed syntax of min options
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
no more bonus for E -- with the soft timeout, this punishes everybody -- the bonus was designed for a hard timeout
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
better merging of similar outputs
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
update minimization documentation
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
imported patch sledge_doc_metis_as_prover
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
automatically minimize with Metis when this can be done within a few seconds
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
minimize with Metis if possible
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
|
changeset |
files
|
| Mon, 30 May 2011 15:30:05 +0100 |
paulson |
Workaround for hyperref bug affecting index entries involving the | symbol
|
changeset |
files
|
| Mon, 30 May 2011 13:58:00 +0200 |
bulwahn |
improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
|
changeset |
files
|
| Mon, 30 May 2011 13:57:59 +0200 |
bulwahn |
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
|
changeset |
files
|
| Mon, 30 May 2011 12:20:04 +0100 |
paulson |
merged multiple heads
|
changeset |
files
|
| Mon, 30 May 2011 12:15:17 +0100 |
paulson |
Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler
|
changeset |
files
|
| Sun, 29 May 2011 19:40:56 +0200 |
blanchet |
always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated
|
changeset |
files
|
| Sun, 29 May 2011 19:40:56 +0200 |
blanchet |
normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
|
changeset |
files
|
| Fri, 27 May 2011 21:11:44 +0200 |
krauss |
function tutorial: do not omit termination proof, even when discussing other things
|
changeset |
files
|
| Fri, 27 May 2011 16:45:24 +0200 |
boehmes |
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
|
changeset |
files
|
| Fri, 27 May 2011 10:41:09 +0200 |
blanchet |
document new "try"
|
changeset |
files
|
| Fri, 27 May 2011 10:33:16 +0200 |
blanchet |
tuned comments
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
new timeout section (cf. Nitpick manual)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
cleanup proof text generation code
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
more Sledgehammer documentation updates
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
minor update
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
try both "metis" and (on failure) "metisFT" in replay
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
show time taken for reconstruction
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
unbreak "max_potential" logic
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
more concise output
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
compile
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
repaired theory merging and defined/used helpers
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
make Sledgehammer a little bit less verbose in "try"
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
handle non-auto try cases gracefully in Try Methods
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
handle non-auto try case gracefully in Solve Direct
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
update SML section of documentation
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
handle non-auto try case gracefully in Nitpick
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
handle non-auto try case of Sledgehammer better
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
removed FIXME: "try_methods" doesn't take a clasimpmod, because it needs to generate Isar proof text in case of success and hence needs total control over its arguments
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
renamed "Auto_Tools" "Try"
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
renamed "try" "try_methods"
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
renamed "metis_timeout" to "preplay_timeout" and continued implementation
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
minor fixes to Sledgehammer docs
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
shorten minimizer command further, exploiting until-now-undocumented syntax
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
minor tweaks to the Nitpick documentation
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
added syntax for specifying Metis timeout (currently used only by SMT solvers)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
readded Waldmeister as default to the documentation and other minor changes
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
reintroduced Waldmeister but limit the number of remote threads created
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
minor doc adjustments
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
make output more concise
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
merge timeout messages from several ATPs into one message to avoid clutter
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
mention contributions from LCP and explain metis and metisFT encodings
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
fixed trivial fact detection
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
cleaner handling of equality and proxies (esp. for THF)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
recognize more ATP failures
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
fully support all type system encodings in typed formats (TFF, THF)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
take out Waldmeister from default for now -- success rate too low on Judgment Day
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
document relevance filter a bit more
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
|
changeset |
files
|
| Thu, 26 May 2011 23:21:00 +0200 |
noschinl |
instance inat for complete_lattice
|
changeset |
files
|
| Thu, 26 May 2011 22:02:40 +0200 |
boehmes |
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
|
changeset |
files
|
| Thu, 26 May 2011 20:51:03 +0200 |
hoelzl |
integral strong monotone; finite subadditivity for measure
|
changeset |
files
|
| Thu, 26 May 2011 20:49:56 +0200 |
hoelzl |
composition of convex and measurable function is measurable
|
changeset |
files
|
| Thu, 26 May 2011 17:59:39 +0200 |
hoelzl |
introduce independence of two random variables
|
changeset |
files
|
| Thu, 26 May 2011 17:40:01 +0200 |
hoelzl |
add lemma indep_distribution_eq_measure
|
changeset |
files
|
| Thu, 26 May 2011 14:12:06 +0200 |
hoelzl |
add lemma indep_rv_finite
|
changeset |
files
|
| Thu, 26 May 2011 14:12:03 +0200 |
hoelzl |
generalize setsum_cases
|
changeset |
files
|
| Thu, 26 May 2011 14:12:02 +0200 |
hoelzl |
add lemma borel_0_1_law
|
changeset |
files
|
| Thu, 26 May 2011 14:12:01 +0200 |
hoelzl |
add lemma sigma_sets_singleton
|
changeset |
files
|
| Thu, 26 May 2011 14:12:00 +0200 |
hoelzl |
use abbrevitation events == sets M
|
changeset |
files
|
| Thu, 26 May 2011 14:11:58 +0200 |
hoelzl |
add lemma kolmogorov_0_1_law
|
changeset |
files
|
| Thu, 26 May 2011 14:11:57 +0200 |
hoelzl |
add lemma indep_sets_collect_sigma
|
changeset |
files
|
| Thu, 26 May 2011 09:42:04 +0200 |
bulwahn |
improving code_int setup in Quickcheck_Narrowing; adding partial_term_of class in Quickcheck_Narrowing
|
changeset |
files
|
| Thu, 26 May 2011 09:42:02 +0200 |
bulwahn |
extending terms of Code_Evaluation by Free to allow partial terms
|
changeset |
files
|
| Thu, 26 May 2011 00:20:28 +0200 |
krauss |
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
|
changeset |
files
|
| Thu, 26 May 2011 00:12:30 +0200 |
krauss |
css rules for highlighting sendback text
|
changeset |
files
|
| Thu, 26 May 2011 00:12:01 +0200 |
krauss |
invert event propagation flag -- in lobobrowser api, true means re-propagate
|
changeset |
files
|
| Wed, 25 May 2011 08:31:36 +0200 |
blanchet |
eta-expand to make SML/NJ happy
|
changeset |
files
|
| Tue, 24 May 2011 18:04:23 +0200 |
blanchet |
ensure that the argument of logical negation is enclosed in parentheses in THF mode
|
changeset |
files
|
| Tue, 24 May 2011 17:05:29 +0200 |
blanchet |
hack to obtain potable step names from Waldmeister
|
changeset |
files
|
| Tue, 24 May 2011 17:04:35 +0200 |
blanchet |
respect user's intention better when setting the CNF_UEQ type system (esp. w.r.t. "erased")
|
changeset |
files
|
| Tue, 24 May 2011 13:29:32 +0200 |
blanchet |
further reduce the number of facts passed to less used remote ATPs
|
changeset |
files
|
| Tue, 24 May 2011 11:55:59 +0200 |
blanchet |
added quietness flag
|
changeset |
files
|
| Tue, 24 May 2011 10:03:15 +0200 |
blanchet |
pass fewer relevant facts to less used remote systems
|
changeset |
files
|
| Tue, 24 May 2011 10:01:03 +0200 |
blanchet |
more work on parsing LEO-II proofs and extracting uses of extensionality
|
changeset |
files
|
| Tue, 24 May 2011 10:01:00 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 24 May 2011 10:00:38 +0200 |
blanchet |
more work on parsing LEO-II proofs without lambdas
|
changeset |
files
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
slightly gracefuller handling of LEO-II and Satallax output
|
changeset |
files
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
document primitive support for LEO-II and Satallax
|
changeset |
files
|