Re: [isabelle] tools on Isabelle.

On Thu, 14 Apr 2011, li yongjian wrote:

1. Is there any proof script tranforming tool from old version to new version. Isabelle has been updated very quickly. But it does not support the old version of proof scripts. For instance, constdefs command is not supported by the new version. I want to ask whether a tool is available to transfer the old proof script into new one supported by the new version of Isabelle.

There is a 6-10 months release cycle. Legacy features like 'constdefs' usually take 1-3 releases from the first indication that they are discontinued (by issuing certain warnings) to removal. This gives more than 1-2 years to update existing theories. This typically becomes unconfortable when NEWS about changes and legacy warnings are ignored for a long time, and you are forced to convert in the last moment, when old features are finally deleted.

2. Mercurial repository.
  Isabelle's development uses Mercury as version control tool.
  Now is it possible to download the most recent version of some materials?
  Is it readable for a user who is not a developper?
  What command to use?

"Using" the repository version is quite adventurous. You need to make yourself an expert of the build process, and the only guarantee is that there will be really many changes in a short time. If you need your thrill every morning instead of working productively, you can start with README_REPOSITORY and Admin/makedist from


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