Re: [isabelle] Syntax for theory definitions
Tjark Weber wrote:
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.
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and