Re: [isabelle] converting to Isar format

On Mon, 21 Aug 2006, Joao Marcos wrote:

>  *** Undeclared class: "logic"
>  *** in arity for type "o"
>  Exception- ERROR raised

This has nothing to do with Isar vs. non-Isar theories -- the actual 
content is the same for both formats.

The above error indicates that class "logic" no longer exists.  Just 
delete the corresponding 'arities' declaration.

> Is there a set of simple rules for translating old theories to the Isar 
> file format?

Whenever Isabelle reports a problem with (outer) syntax, check the 
diagrams given in the Isar reference manual.  After some practice you 
should be able to see the few patterns of changes required for your 
particular theories.  The appendix of the manual also gives some hints on 
converting proof scripts -- use this together with ``isatool convert''.


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