Re: [isabelle] Syntax for theory definitions



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 archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.