# HG changeset patch
# User kleing
# Date 1104984926 -3600
# Node ID 3f1a674b7ec714b2b164b78cf609b18859059135
# Parent  4b939ba65c31e5bb6b5cc4d8384676a1b0d127bb
suggestions by Jeremy Siek

diff -r 4b939ba65c31 -r 3f1a674b7ec7 doc-src/LaTeXsugar/Sugar/LaTeXsugar.thy
--- 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:\_>")
diff -r 4b939ba65c31 -r 3f1a674b7ec7 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- 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}!\\