Re: [isabelle] LNCS format and isatool



Dear Peter,

I have never encountered a similar problem (using LLNCS DOCUMENT CLASS
-- version 2.14 (17-Aug-2004)).

> Now, I have found the \def command to which this error refers (l.57 is
> just a blank line), and it is in the .tex file created by the
> combination of the Isabelle markup and LaTeX markup in my .thy file. 
> Specifically, it is this line
> 
> %
> \begin{isabellebody}%
> \def\isabellecontext{Craignd}%
> %
> \isadelimtheory
> %
> \endisadelimtheory
> %
> \isatagtheory
> %
> \endisatagtheory
> {\isafoldtheory}%
> %

I dont't think that the problem is in this \def -- maybe it is a strange
interference between different parts of the TeX soup.  Perhaps some
changes / deletetions in the generated TeX (directory generated/) may
yield a more precise error description.

Hope this helps
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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