--- 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 *}