Fri, 27 May 2011 21:11:44 +0200 krauss function tutorial: do not omit termination proof, even when discussing other things
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
Fri, 27 May 2011 10:41:09 +0200 blanchet document new "try"
Fri, 27 May 2011 10:33:16 +0200 blanchet tuned comments
Fri, 27 May 2011 10:30:08 +0200 blanchet new timeout section (cf. Nitpick manual)
Fri, 27 May 2011 10:30:08 +0200 blanchet cleanup proof text generation code
Fri, 27 May 2011 10:30:08 +0200 blanchet more Sledgehammer documentation updates
Fri, 27 May 2011 10:30:08 +0200 blanchet minor update
Fri, 27 May 2011 10:30:08 +0200 blanchet try both "metis" and (on failure) "metisFT" in replay
Fri, 27 May 2011 10:30:08 +0200 blanchet show time taken for reconstruction
Fri, 27 May 2011 10:30:08 +0200 blanchet unbreak "max_potential" logic
Fri, 27 May 2011 10:30:08 +0200 blanchet more concise output
Fri, 27 May 2011 10:30:08 +0200 blanchet compile
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)
Fri, 27 May 2011 10:30:08 +0200 blanchet repaired theory merging and defined/used helpers
Fri, 27 May 2011 10:30:08 +0200 blanchet make Sledgehammer a little bit less verbose in "try"
Fri, 27 May 2011 10:30:08 +0200 blanchet handle non-auto try cases gracefully in Try Methods
Fri, 27 May 2011 10:30:08 +0200 blanchet handle non-auto try case gracefully in Solve Direct
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
Fri, 27 May 2011 10:30:08 +0200 blanchet update SML section of documentation
Fri, 27 May 2011 10:30:08 +0200 blanchet handle non-auto try case gracefully in Nitpick
Fri, 27 May 2011 10:30:08 +0200 blanchet handle non-auto try case of Sledgehammer better
Fri, 27 May 2011 10:30:08 +0200 blanchet added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
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
Fri, 27 May 2011 10:30:08 +0200 blanchet renamed "Auto_Tools" "Try"
Fri, 27 May 2011 10:30:08 +0200 blanchet removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
Fri, 27 May 2011 10:30:08 +0200 blanchet renamed "try" "try_methods"
Fri, 27 May 2011 10:30:08 +0200 blanchet renamed "metis_timeout" to "preplay_timeout" and continued implementation
Fri, 27 May 2011 10:30:08 +0200 blanchet minor fixes to Sledgehammer docs
Fri, 27 May 2011 10:30:08 +0200 blanchet shorten minimizer command further, exploiting until-now-undocumented syntax
Fri, 27 May 2011 10:30:07 +0200 blanchet minor tweaks to the Nitpick documentation
Fri, 27 May 2011 10:30:07 +0200 blanchet added syntax for specifying Metis timeout (currently used only by SMT solvers)
Fri, 27 May 2011 10:30:07 +0200 blanchet readded Waldmeister as default to the documentation and other minor changes
Fri, 27 May 2011 10:30:07 +0200 blanchet reintroduced Waldmeister but limit the number of remote threads created
Fri, 27 May 2011 10:30:07 +0200 blanchet renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
Fri, 27 May 2011 10:30:07 +0200 blanchet minor doc adjustments
Fri, 27 May 2011 10:30:07 +0200 blanchet make output more concise
Fri, 27 May 2011 10:30:07 +0200 blanchet merge timeout messages from several ATPs into one message to avoid clutter
Fri, 27 May 2011 10:30:07 +0200 blanchet fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
Fri, 27 May 2011 10:30:07 +0200 blanchet tuning
Fri, 27 May 2011 10:30:07 +0200 blanchet mention contributions from LCP and explain metis and metisFT encodings
Fri, 27 May 2011 10:30:07 +0200 blanchet fixed trivial fact detection
Fri, 27 May 2011 10:30:07 +0200 blanchet cleaner handling of equality and proxies (esp. for THF)
Fri, 27 May 2011 10:30:07 +0200 blanchet recognize more ATP failures
Fri, 27 May 2011 10:30:07 +0200 blanchet fully support all type system encodings in typed formats (TFF, THF)
Fri, 27 May 2011 10:30:07 +0200 blanchet take out Waldmeister from default for now -- success rate too low on Judgment Day
Fri, 27 May 2011 10:30:07 +0200 blanchet document relevance filter a bit more
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)
Fri, 27 May 2011 10:30:07 +0200 blanchet towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
Thu, 26 May 2011 23:21:00 +0200 noschinl instance inat for complete_lattice
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)
Thu, 26 May 2011 20:51:03 +0200 hoelzl integral strong monotone; finite subadditivity for measure
Thu, 26 May 2011 20:49:56 +0200 hoelzl composition of convex and measurable function is measurable
Thu, 26 May 2011 17:59:39 +0200 hoelzl introduce independence of two random variables
Thu, 26 May 2011 17:40:01 +0200 hoelzl add lemma indep_distribution_eq_measure
Thu, 26 May 2011 14:12:06 +0200 hoelzl add lemma indep_rv_finite
Thu, 26 May 2011 14:12:03 +0200 hoelzl generalize setsum_cases
Thu, 26 May 2011 14:12:02 +0200 hoelzl add lemma borel_0_1_law
Thu, 26 May 2011 14:12:01 +0200 hoelzl add lemma sigma_sets_singleton
Thu, 26 May 2011 14:12:00 +0200 hoelzl use abbrevitation events == sets M
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip