Email Gateway (Mar 26 2025 at 00:26): Email Gateway (Mar 26 2025 at 00:26):From: Peter Hoefner <cl-isabelle-users@lists.cam.ac.uk>
Hi all,
It seems that the standard Isabelle packages (Isabelle.sty,isabellesym.sty) do not work with the package comment.
Minimal working example attached (comment in line 3 to see error message).
This is problematic since the document class of lipics requires comment.
Cheers
Peter
%\documentclass{lipics-v2021}
\documentclass{article}
% \usepackage{comment} % <-- breaks if package comment is used;
% this package is used in lipics document class
\usepackage{isabelle,isabellesym}
\begin{document}
\begin{isabelle}
something
\isadelimproof
% %
\endisadelimproof
\end{isabelle}
\end{document}
Email Gateway (Mar 26 2025 at 10:29):From: Makarius <makarius@sketis.net>
On 26/03/2025 01:25, Peter Hoefner (via cl-isabelle-users Mailing List) wrote:
Hi all,
It seems that the standard Isabelle packages (Isabelle.sty,isabellesym.sty) do
not work with the package comment.
Minimal working example attached (comment in line 3 to see error message).
This is problematic since the document class of lipics requires comment.
The Isabelle document preparation system requires the "comment" package on its
own account. It uses it in PlainTeX mode as follows:
%plain TeX version of comment package -- much faster!
\let\isafmtname\fmtname\def\fmtname{plain}
\usepackage{comment}
\let\fmtname\isafmtname
The regular LaTeX setup is available via "options [document_comment_latex]" in
the session ROOT configuration.
(One happy day I will remove the need for "comment" in Isabelle document
output, and just do it directly in Isabelle/Scala instead of odd TeX programming.)
Makarius
Last updated: May 30 2025 at 04:27 UTC