Hernán Rajchert (Feb 28 2023 at 13:50): Hernán Rajchert (Feb 28 2023 at 13:50):Hi! I'm tryign to pretty print an inference rule, and I'm using as reference the examples provided in the Sugar latex document. My conclusion is rather long and it breaks the line
Screen-Shot-2023-02-28-at-10.43.51.png
Looking at the Mathpartir documentation, I should be able to force a line break by inserting a \\, but I'm not sure if I'm able to use that with this definition
text
‹
\begin{center}
@{thm[mode=Rule,margin=100] IfFalse} {\sc IfFalse}
\end{center}
›
I tried looking at the source that produces the inference rules for Big Step semantics in the concrete semantics book, but it doesn't seem to live under the BigStep theory. Are there available any complex examples to see how can I modify the output?
Wolfgang Jeltsch (Feb 28 2023 at 14:39):Without having looked at the details at all, let me just throw into the discussion that within inner syntax snippets (types, terms) you can add additional LaTeX code with the latex antiquotation. See Subsection 3.3.5 (_Document comments_) in the Isabelle/Isar Reference Manual.
Last updated: Apr 28 2024 at 12:28 UTC