Re: [isabelle] help on Trueprop

Many thanx for the quick reply.  I definitely need to study the
isar-ref manual carefully.  I wish there was somewhere a summary "for
dummies" of all the modifications introduced by the new theory

Now, the declarations I had for Trueprop and TruepropExt were the following:

 Trueprop       :: [seq'=>seq',seq'=>seq']=>prop
 TruepropExt    :: [seq,seq]=>prop          ("((_)/ |- (_))" [6,6] 5)

The error message I now get, when reading my theory after taking your
explanation about the pervasiveness of Sequents, is the following:

 ### Non-Isar file format for theory "SPROP" -- deprecated
 *** Illegal occurrence of syntactic type: "seq"
 *** The error(s) above occurred in type "[seq , seq ] => prop "
 *** in declaration of constant "TruepropExt"
 Exception- ERROR raised
 Exception- ERROR raised

I have opened both Sequents.thy and the isar-ref manual to see if I
can understand, but I still wonder: what in the world has happened
with the type "seq"??

Thanks in advance, again, for the help.  Best,

On 9/6/06, Makarius <makarius at> wrote:
On Tue, 5 Sep 2006, Joao Marcos wrote:

>  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"))]

As usual, fgrep -r will do the job:

> fgrep -r  two_seq_tr Isabelle2005/src/Sequents
Isabelle2005/src/Sequents/ILL.thy:   ("@Context", two_seq_tr "Context"),
Isabelle2005/src/Sequents/ILL.thy:   ("Context", two_seq_tr'"@Context"),
Isabelle2005/src/Sequents/LK0.thy:parse_translation {* [("@Trueprop", two_seq_tr "Trueprop")] *}
Isabelle2005/src/Sequents/LK0.thy:print_translation {* [("Trueprop", two_seq_tr' "@Trueprop")] *}
Isabelle2005/src/Sequents/Sequents.thy:fun two_seq_tr c [s1,s2] =
Isabelle2005/src/Sequents/Sequents.thy:fun two_seq_tr' c [s1, s2] =

In other words these ML translations functions are now pervasive, the
Sequents structure has disappeared.

BTW, any kind of ML programming works much better with the new theory
format.  Just use the commands 'print_translation' or 'parse_translation'
here (see also the isar-ref manual).


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