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
> more!

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:

theory P_is_NP
imports HOLF
begin

theorem P_is_NP: "P = NP"
by exfalso

end

Simply amazing!

- Brian




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.