Re: [isabelle] Announcement: Isabelle/HOLF



Hi Lars.

A really nice work. I do not want to use any other Isabelle-Logic any
more!

Here are some first impressions and suggestions for improvement:

1) I'm really missing sledgehammer. I have a problem to prove the
following theorem, which is an old challenge problem from a leading CPU
manufacturer:
  theorem fpu_correct: "1.0 + 1.0 = 3.0" 

Due to my understanding, the Falso-Logic should be able to prove it.
However, when I tried sledgehammer, it does not find a proof? Any hints?

2) For some really nasty Isabelle-Hacking, that I do not dare to
reproduce on this list, a lemma of the following form would be nice:
  lemma: "PROP P"

However, my attempt to prove that "by exfalso" failed. Any chance to
extend the proof method such that it also proves this lemma?

Thanks again for this really great hack,
  Peter










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