--- a/src/HOL/Examples/ML.thy Thu Jun 11 14:13:04 2020 +0200
+++ b/src/HOL/Examples/ML.thy Thu Jun 11 14:18:34 2020 +0200
@@ -5,7 +5,7 @@
section \<open>Isabelle/ML basics\<close>
theory "ML"
-imports Main
+ imports Main
begin
subsection \<open>ML expressions\<close>
--- a/src/HOL/Examples/Seq.thy Thu Jun 11 14:13:04 2020 +0200
+++ b/src/HOL/Examples/Seq.thy Thu Jun 11 14:18:34 2020 +0200
@@ -5,7 +5,7 @@
section \<open>Finite sequences\<close>
theory Seq
-imports Main
+ imports Main
begin
datatype 'a seq = Empty | Seq 'a "'a seq"
--- a/src/Tools/SML/Examples.thy Thu Jun 11 14:13:04 2020 +0200
+++ b/src/Tools/SML/Examples.thy Thu Jun 11 14:18:34 2020 +0200
@@ -5,7 +5,7 @@
section \<open>Standard ML within the Isabelle environment\<close>
theory Examples
-imports Pure
+ imports Pure
begin
text \<open>