[isabelle] LNCS format and isatool

Hi


I'm trying to use the isatool document preparation system in conjunction with the LNCS LaTeX class file. When I use a normal "article" class file, the build works fine, and produces the correct document with no errors. When I change to \documentclass{llncs} and try the same thing, I get 100+ fatal errors, each of which is

! Paragraph ended before \def was complete.
\par
l.57

(That makes 100 errors; please try again.)
!  ==> Fatal error occurred, no output PDF file produced!
Transcript written on root.log.


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}%
%
%
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%


(my bold) which is right at the top of the file. Has anyone come across this problem before when trying to combine an Isabelle build with the LNCS class file? Or does anyone know how to fix it?

If it helps, here is the class file

Many thanks

Peter



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