Lawrence Paulson writes:
Florian has suggested making sledgehammer available earlier in the
construction of Main, before PreList at least. This could be useful
to developers. However, it requires Hilbert_Choice, which must also
be introduced earlier. We previously put some effort
Florian has suggested making sledgehammer available earlier in the
construction of Main, before PreList at least. This could be useful
to developers. However, it requires Hilbert_Choice, which must also
be introduced earlier.
A PreList-Sledgehammer would be a nice thing to have, but it
It needs at least Hilbert_Choice. It could go before Datatype. Some
details need to be worked out to ensure that all theorems in Main.thy
get converted to clause form.
Larry
On 14 Sep 2007, at 14:46, Florian Haftmann wrote:
A PreList-Sledgehammer would be a nice thing to have, but it is not
Lawrence Paulson wrote:
It needs at least Hilbert_Choice. It could go before Datatype. Some
details need to be worked out to ensure that all theorems in Main.thy
get converted to clause form.
I must confess that I have lost track now. Does only the skolemization
depend on Hilbert-Choice, or
On Fri, 14 Sep 2007, Stefan Berghofer wrote:
For those members of the list who have not followed the discussion
about this issue a few years ago, let me cite what Larry wrote about it:
I think it would be quite easy to do, and sensible (ZF has always been
that way).
[...]
If
