Re: [isabelle] LNCS format and isatool



I am doing this all the time (incl yesterday). If I had a problem at some point, I have forgotten. I just checked, I am using the latest llncs.cls (which seems not to have changed in a while). I have appended how my roo.tex starts.

Sorry not to be of more help,
Tobias

\documentclass[envcountsame]{llncs}
\usepackage{isabelle,isabellesym}
\usepackage{amssymb}
\usepackage[latin1]{inputenc}
% this should be the last package used
\usepackage{pdfsetup}
% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

\begin{document}
\pagestyle{plain}
\title{Linear Quantifier Elimination}
\author{Tobias Nipkow}
\authorrunning{T. Nipkow}
\institute{Institut fr Informatik, Technische Universitt Mnchen}

\date{}
\maketitle

...

\input{session}

Peter Chapman wrote:
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.
<to be read again>
                   \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}%
%
\isadelimtheory
%
\endisadelimtheory
%
\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.