Isabelle 2007 released

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 a \in A  A\subseteq B have a \in B

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.



Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: