[Logiweb] Diagnose error

[Kasper H0st Frederiksen]

We all remember the warning that, if you write a proof line that uses
a double successor operation you have to remenber to write (b')' not b''.

Now, if line L1 uses the correct form: (b')', and you want to use 
L1 in another line L2(f.eks for a modus ponens), AND you make a 
mistake while typing L2 then pyk shoule provede a diagnose page with a 
'Lemma/Proof mismatch -error', but it does not. The diagnose dvi file is 
corrupted but the body file is fine. Latex says this is because of a 
double superscript error.

I am not 100% shure this is the correct interpretation of the problem, but 
I have uptoaded a page that ilustrates the error
http://www.diku.dk/~grue/logiweb/20050502/home/tofu/diagnose-error/fixed/

The body is corectly complied and the diagnose is corrupt.
If you correct line eight of the last proof (or remove the line) you get a 
readable diagnose file.