Re: [isabelle] Syntax for theory definitions



Tjark Weber wrote:
Devrim,

On Tue, 2008-09-23 at 14:15 +0300, Devrim Ünal wrote:
I want to run Isabelle over some theories developed by another
researcher. I downloaded
the theories but can not run them in Isabelle 2008.

Any comments on how I can run/convert them so that they work in Isabelle 2008?

converting theories can be a daunting task (especially if they are very
old or very large).  You can try running "isatool fixheaders", but if
you still get error messages afterward that you cannot fix easily, I
have another suggestion: how about installing the version of Isabelle
that these theories were originally developed for?  Old Isabelle
releases are available from
http://www.cl.cam.ac.uk/research/hvg/Isabelle/download_past.html

Best,
Tjark

This is, at best, only a partial solution. I've done a mass of work recently in Isabelle2005 because it's built on other stuff which works on Isabelle2005. But what happens when I want to combine it with someone else's theories which are written in Isabelle2007? This looks like being a serious problem for me. On a similar theme, I have been recently helping a colleague who wants to get some familiarity with Isabelle. He found some tutorial material on the web somewhere, but it didn't work. Why? Because it was written before the changes made in Isabelle2007. We had to revert to Isabelle2005 to run it.

Yesterday, he was trying to run a different lot of tutorial material which he had found somewhere. It didn't work either, because it used a form of syntax I've never seen before. I would guess it's Isabelle2008 (which I've never used). (It's primrec statement is totally different from anything I've seen in the last 10 years).

These issues seem to be capable of causing massive and unnecessary difficulties.

Jeremy







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