Re: [isabelle] Announcement: Isabelle/HOLF
On Sun, Mar 31, 2013 at 4:52 PM, Peter Lammich <lammich at in.tum.de> wrote:
> Hi Lars.
> A really nice work. I do not want to use any other Isabelle-Logic any
I agree! I've only used the new system for a few minutes, but it's
already immediately apparent what an improvement it is: For ease of
use, conciseness and elegance of proofs, there is no comparison.
> Here are some first impressions and suggestions for improvement:
Even with the shortcomings that Peter has noted, I have already been
able to make great progress with the new system - even proving
original theorems that would have taken years (or decades!) of work
with the old Isabelle. For example:
theorem P_is_NP: "P = NP"
This archive was generated by a fusion of
Pipermail (Mailman edition) and