Stream: Beginner Questions

Topic: Can I customize the generated inference rule?

view this post on Zulip 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


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


  @{thm[mode=Rule,margin=100] IfFalse} {\sc IfFalse}

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?

view this post on Zulip 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: Feb 27 2024 at 08:17 UTC