# HG changeset patch
# User Andreas Lochbihler
# Date 1380277599 -7200
# Node ID ea38710e731c15e3792567d16666ea0169890364
# Parent  021a8ef97f5f50c4f28343ff67f61b55dcffebeb# Parent  2a4c156e6d367f71d78b002f460f8f4823290a5d
merged

diff -r 021a8ef97f5f -r ea38710e731c src/HOL/ex/ML.thy
--- a/src/HOL/ex/ML.thy	Fri Sep 27 12:26:23 2013 +0200
+++ b/src/HOL/ex/ML.thy	Fri Sep 27 12:26:39 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 *}