# HG changeset patch
# User wenzelm
# Date 1380275812 -7200
# Node ID 2a4c156e6d367f71d78b002f460f8f4823290a5d
# Parent  54b08afc03c762706e9d04f1552cee9448a6795f
proper latex;

diff -r 54b08afc03c7 -r 2a4c156e6d36 src/HOL/ex/ML.thy
--- a/src/HOL/ex/ML.thy	Fri Sep 27 10:40:02 2013 +0200
+++ b/src/HOL/ex/ML.thy	Fri Sep 27 11:56:52 2013 +0200
@@ -55,9 +55,11 @@
 text {*
   ML embedded into the Isabelle environment is connected to the Prover IDE.
   Poly/ML provides:
-    \<bullet> precise positions for warnings / errors
-    \<bullet> markup for defining positions of identifiers
-    \<bullet> markup for inferred types of sub-expressions
+  \begin{itemize}
+    \item precise positions for warnings / errors
+    \item markup for defining positions of identifiers
+    \item markup for inferred types of sub-expressions
+  \end{itemize}
 *}
 
 ML {* fn i => fn list => length list + i *}