Re: [isabelle] help on Trueprop

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.