--- a/src/Doc/Sugar/Sugar.thy Thu Aug 03 19:10:36 2023 +0200
+++ b/src/Doc/Sugar/Sugar.thy Thu Aug 03 19:10:43 2023 +0200
@@ -231,6 +231,25 @@
Instead of a single variable \verb!z! you can give a whole list \verb!x y z!
to perform multiple $\eta$-expansions.
+
+\subsection{Breaks and boxes}
+
+Printing longer formulas can easily lead to line breaks in unwanted places.
+This can be avoided by putting \LaTeX-like mboxes in formulas.
+There is a function @{const_typ mbox} that you can wrap around subterms and that
+is pretty-printed as a \LaTeX\ \verb$\mbox{ }$.
+If you are printing a term or formula, you can just insert @{const mbox}
+wherever you want. You can also insert it into theorems by
+virtue of the fact that @{const mbox} is defined as an identity function. Of course
+you need to adapt the proof accordingly.
+
+Unless the argument of @{const mbox} is an identifier or an application (i.e.\ of the highest precedence),
+it will be enclosed in parentheses. Thus \verb!x < mbox(f y)! results in @{term "x < mbox(f y)"}
+but \verb!x < mbox(y+z)! results in @{term "x < mbox(y+z)"}. You can switch off the
+parentheses by using the variant @{const mbox0} instead of @{const mbox}:
+\verb!x < mbox0(y+z)! results in @{term "x < mbox0(y+z)"}.
+
+
\subsection{Inference rules}
To print theorems as inference rules you need to include Didier
--- a/src/HOL/Library/LaTeXsugar.thy Thu Aug 03 19:10:36 2023 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy Thu Aug 03 19:10:43 2023 +0200
@@ -8,6 +8,18 @@
imports Main
begin
+(* Boxing *)
+
+definition mbox :: "'a \<Rightarrow> 'a" where
+"mbox x = x"
+
+definition mbox0 :: "'a \<Rightarrow> 'a" where
+"mbox0 x = x"
+
+notation (latex) mbox ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>" [999] 999)
+
+notation (latex) mbox0 ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>" [0] 999)
+
(* LOGIC *)
notation (latex output)
If ("(\<^latex>\<open>\\textsf{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>else\<^latex>\<open>}\<close> (_))" 10)
--- a/src/HOL/Tools/SMT/cvc5_replay_methods.ML Thu Aug 03 19:10:36 2023 +0200
+++ b/src/HOL/Tools/SMT/cvc5_replay_methods.ML Thu Aug 03 19:10:43 2023 +0200
@@ -108,7 +108,7 @@
else if r = Lethe_Proof.th_resolution_rule then Theory_Resolution
else if r = Lethe_Proof.equiv_pos2_rule then Equiv_pos2
else if r = Lethe_Proof.hole orelse r = "undefined" then Hole
- else (@{print} ("maybe unsupported rule", r); Other_Rule r)
+ else Other_Rule r
fun normalized_input ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
let