# HG changeset patch
# User wenzelm
# Date 1591649346 -7200
# Node ID 73ff22f99d3825a6e218bca1e3c14030dd918ddf
# Parent  ae643fb4ca30ef17fb57ab98e892e1f897b2b72e
tuned document;

diff -r ae643fb4ca30 -r 73ff22f99d38 src/HOL/Examples/ML.thy
--- a/src/HOL/Examples/ML.thy	Mon Jun 08 22:31:36 2020 +0200
+++ b/src/HOL/Examples/ML.thy	Mon Jun 08 22:49:06 2020 +0200
@@ -8,7 +8,7 @@
 imports Main
 begin
 
-section \<open>ML expressions\<close>
+subsection \<open>ML expressions\<close>
 
 text \<open>
   The Isabelle command \<^theory_text>\<open>ML\<close> allows to embed Isabelle/ML source into the
@@ -27,7 +27,7 @@
 ML \<open>val c = a + b\<close>
 
 
-section \<open>Antiquotations\<close>
+subsection \<open>Antiquotations\<close>
 
 text \<open>
   There are some language extensions (via antiquotations), as explained in the
@@ -57,7 +57,7 @@
 \<close>
 
 
-section \<open>Recursive ML evaluation\<close>
+subsection \<open>Recursive ML evaluation\<close>
 
 ML \<open>
   ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>;
@@ -67,7 +67,7 @@
 \<close>
 
 
-section \<open>IDE support\<close>
+subsection \<open>IDE support\<close>
 
 text \<open>
   ML embedded into the Isabelle environment is connected to the Prover IDE.
@@ -84,7 +84,7 @@
 ML \<open>fn i => fn list => length list + i\<close>
 
 
-section \<open>Example: factorial and ackermann function in Isabelle/ML\<close>
+subsection \<open>Example: factorial and ackermann function in Isabelle/ML\<close>
 
 ML \<open>
   fun factorial 0 = 1
@@ -105,7 +105,7 @@
 ML \<open>timeit (fn () => ackermann 3 10)\<close>
 
 
-section \<open>Parallel Isabelle/ML\<close>
+subsection \<open>Parallel Isabelle/ML\<close>
 
 text \<open>
   Future.fork/join/cancel manage parallel evaluation.
@@ -130,7 +130,7 @@
 ML \<open>timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10))\<close>
 
 
-section \<open>Function specifications in Isabelle/HOL\<close>
+subsection \<open>Function specifications in Isabelle/HOL\<close>
 
 fun factorial :: "nat \<Rightarrow> nat"
 where
diff -r ae643fb4ca30 -r 73ff22f99d38 src/HOL/Examples/document/root.tex
--- a/src/HOL/Examples/document/root.tex	Mon Jun 08 22:31:36 2020 +0200
+++ b/src/HOL/Examples/document/root.tex	Mon Jun 08 22:49:06 2020 +0200
@@ -15,6 +15,8 @@
 \title{Notable Examples in Isabelle/HOL}
 \maketitle
 
+\tableofcontents
+
 \parindent 0pt \parskip 0.5ex
 
 \input{session}