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