Re: [isabelle] documentation



Hi Stefania,

the first error mistake is at line 10051.

It seems that you have (accidentally?) put some Isar text into text {*
*} sections, upon which tex will choke of course.

To debug such tex issues it can also be helpful to run tex manually on
the generated sources, usually by switching to the directory with the
generated sources and running pdflatex root.tex or something alike.

Hope this helps
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

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.