Re: [isabelle] Syntax for theory definitions


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


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