[isabelle] converting to Isar format



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





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