[isabelle] help on Trueprop



Dear ALL:

We still have some trouble adapting some theories that we have
developed for Isabelle 2004 so as to make them work in the 2005
distribution.  Specifically, this time we had a reformulation of the
classic theory of sequents that initiates with:

 SPROP = Sequents +
 ...

The thing is that we use at the end of the file two lines of ML code
intended to translate in between the internal and the external
representation of sequents in Isabelle, namely:

 val parse_translation = [("TruepropExt",Sequents.two_seq_tr "Trueprop")];
 val print_translation = [("Trueprop",Sequents.two_seq_tr' "TruepropExt")];

But these do not work anymore.  When we call our theory SPROP.thy
inside Isabelle we receive the message:


 Loading theory "SPROP"
 ### Non-Isar file format for theory "SPROP" -- deprecated
 Error: in '/tmp/isabelle-jmarcos5522/SPROP_thy.ML', line 14.
 Structure (Sequents) has not been declared
 Found near [ ( "TruepropExt", Sequents.two_seq_tr("Trueprop"))]

 Error: in '/tmp/isabelle-jmarcos5522/SPROP_thy.ML', line 15.
 Structure (Sequents) has not been declared
 Found near [ ( "Trueprop", Sequents.two_seq_tr'("TruepropExt"))]

 Exception- Fail "Static errors (pass2)" raised


Can anyone suggest a corrective measure?

Thanx in advance!
Joao Marcos





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