Email Gateway (Aug 18 2022 at 09:33): Email Gateway (Aug 18 2022 at 09:33):From: Joao Marcos <jmarcos@dimap.ufrn.br>
Dear All:
I have always been using Isabelle 2004, and wrote all my theories
(basically, a collection of non-classical logics, in various formats)
for it. Recently, though, I have installed the new distribution,
Isabelle 2005, for the first time. The message I consistently receive
when trying to use my old theories, say, my theory "PROPOSICIONAL",
is:
Loading theory "PROPOSICIONAL"
### Non-Isar file format for theory "PROPOSICIONAL" -- deprecated
*** Undeclared class: "logic"
*** in arity for type "o"
Exception- ERROR raised
Exception- ERROR raised
Is there a set of simple rules for translating old theories to the
Isar file format? I have seen a few comments about the new headers at
the Isabelle web-site and comments about the "rules" section
transforming into "axioms". Is that all? Can anyone give me hints to
ease the conversion?
Thanx in advance! Best,
Joao Marcos
Email Gateway (Aug 18 2022 at 09:33):From: Makarius <makarius@sketis.net>
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''.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC