On Fri, 27 Apr 2012, Christian Sternagel wrote:
Maybe I should have tried it myself before posting ;). Yes, it works
with jdk1.6.0_32.
The test website already provides the bundled JDK, which is jdk1.6.0_31
and was produced just before Oracle upgraded to 32 :-(
Fortunately there are hardly
Hi all,
With the latest Isabelle (44b33c1e702e), some attributes, e.g. unify_search
bound, give pairs of spurious warnings, e.g.
### Ignoring local change of global option unify_search_bound
even when they are declared globally, as in the theory below:
theory Scratch
imports Main
On Fri, 27 Apr 2012, Jasmin Christian Blanchette wrote:
With the latest Isabelle (44b33c1e702e), some attributes, e.g.
unify_search bound, give pairs of spurious warnings, e.g.
### Ignoring local change of global option unify_search_bound
even when they are declared globally, as in the
On Tue, 24 Apr 2012, Makarius wrote:
I have also made some more experiments. The Empty exception is from the
split_last here
http://isabelle.in.tum.de/repos/isabelle/file/ea153f6abdb6/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML#l614
where you don't get any output unexpectedly, bacause
