The Isabelle team has released Isabelle2007. The best news is that although I am probably the only Isabelle user that uses the ZF logic, it is still maintained and nothing got broken.

The changelog does not mention ZF at all. However, there are certain changes that affect IsarMathLib in a good way. The most important are improvements in automatic proving tactics. I have rewritten some theorems from the IsarMathLib’s Semigroup_ZF theory file with a new terminology and the proofs can be made about 30% shorter in Isabelle2007 than Isabelle2005. Sometimes it is getting to the point that I worry that the proofs are becoming too terse.

Other interesting things that I noticed are the **definition** keyword that replaces **constdefs ** and possibility of refering to known facts as literal propositions. This means we can write

**from** **have**

instead of refering to known facts through labels that the reader has to locate in the proof to find out what they mean.

What is still lacking is a good HTML presentation of the formalized mathematical text. The current Isabelle – generated files show very little of mathematical notation and completely ignore notation defined in locales.

### Like this:

Like Loading...

*Related*

Tags: Isabelle

This entry was posted on November 25, 2007 at 2:56 am and is filed under news. You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.

## Leave a Reply