[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Latex printing. a problem.



Hi Mauro,

As described in the system manual, page 46, the theory.tex files are
intended to be included in another latex document and are not standalone
documents.  In addition to those files, a "pvs-files.tex" file should have
been generated that includes the theory.tex files and may be latexed.  It
also serves as an example of what is needed to include these in your own
documents.

Hope this helps,

Sam Owre

> From:    Mauro Gargano <maurogargano@inwind.it>
> Subject: Latex printing. a problem.
> Date:    Tue, 08 Jan 2002 19:21:41 +0100
> To:      pvs-help@csl.sri.com
> 
> [1  <text/plain; us-ascii (7bit)>]
> Hello,
> 
> I have problem to transform the .tex file generated by pvs in .dvi
> files.
> iI use the PVS > PRINTING > LATEX-PVS-FILE to generate the pvs, than I
> lunch "latex  filename.tex" and the latex program starts to complain
> that
> 
> 
>           This is TeX, Version 3.14159 (Web2C 7.3.1)
> 
>           (spec_u7.tex
> 
>           LaTeX2e <2000/06/01>
> 
>           Babel <v3.7h> and hyphenation patterns for american, french, german, ngerman, n
> 
>           ohyphenation, loaded.
> 
>           ! LaTeX Error: Environment alltt undefined.
> 
>           See the LaTeX manual or LaTeX Companion for explanation.
> 
>           Type  H <return>  for immediate help.
> 
>            ...
> 
> 
> 
>           l.35 \begin{alltt}
> 
> 
> 
>           ?
> 
>           ! Emergency stop.
> 
>            ...
> 
> 
> 
>           l.35 \begin{alltt}
> 
> 
> 
>           No pages of output.
> 
>           Transcript written on spec_u7.log.
> 
> Can you please explain me what is the procedure to produce the dvi file
> from the tex file generated by PVS?
> 
> 
> thanks in advance.
> Mauro.
> [2  <text/html; us-ascii (7bit)>]
>