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
://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20070914/fa2278cb/attachment.vcf
-- next part --
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 185 bytes
Desc: OpenPGP digital signature
Url
, but it is not
crucial. Anyway I agree with Tobias that Metis itself should be
offered
as soon as possible. Why not HOL.thy?
-- next part --
An HTML attachment was scrubbed...
URL:
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20070914/b302fbba
, or also metis?
Florian
-- next part --
A non-text attachment was scrubbed...
Name: florian.haftmann.vcf
Type: text/x-vcard
Size: 654 bytes
Desc: not available
Url :
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20070914/c7ec716e
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
