--- a/doc-src/LaTeXsugar/Sugar/LaTeXsugar.thy Thu Jan 06 03:00:58 2005 +0100
+++ b/doc-src/LaTeXsugar/Sugar/LaTeXsugar.thy Thu Jan 06 05:15:26 2005 +0100
@@ -44,7 +44,7 @@
(* nth *)
syntax (latex output)
- nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" ("_\<^raw:$_{[\mathit{>_\<^raw:}]}$>" [1000,0] 1000)
+ nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
(* DUMMY *)
consts DUMMY :: 'a ("\<^raw:\_>")
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu Jan 06 03:00:58 2005 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu Jan 06 05:15:26 2005 +0100
@@ -279,15 +279,14 @@
text_raw {*
\begin{figure}
\begin{center}\begin{minipage}{0.6\textwidth}
- \begin{isabellebody}
+ \isastyle\isamarkuptrue
*}
lemma True
proof -
-- "pretty trivial"
show True by force
qed
-text_raw {*
- \end{isabellebody}
+text_raw {*
\end{minipage}\end{center}
\caption{Example proof in a figure.}\label{fig:proof}
\end{figure}
@@ -299,7 +298,7 @@
\verb!text_raw {!\verb!*!\\
\verb! \begin{figure}!\\
\verb! \begin{center}\begin{minipage}{0.6\textwidth}!\\
-\verb! \begin{isabellebody}!\\
+\verb! \isastyle\isamarkuptrue!\\
\verb!*!\verb!}!\\
\verb!lemma True!\\
\verb!proof -!\\
@@ -307,7 +306,6 @@
\verb! show True by force!\\
\verb!qed!\\
\verb!text_raw {!\verb!*!\\
-\verb! \end{isabellebody}!\\
\verb! \end{minipage}\end{center}!\\
\verb! \caption{Example proof in a figure.}\label{fig:proof}!\\
\verb! \end{figure}!\\