# HG changeset patch
# User wenzelm
# Date 1591877914 -7200
# Node ID 914baafb3da4176b9656f298afa56ac2a0a5967b
# Parent  aec0f7b58cc60b05ec5885c009b653badfdab77d
tuned whitespace;

diff -r aec0f7b58cc6 -r 914baafb3da4 src/HOL/Examples/ML.thy
--- 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>
diff -r aec0f7b58cc6 -r 914baafb3da4 src/HOL/Examples/Seq.thy
--- 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"
diff -r aec0f7b58cc6 -r 914baafb3da4 src/Tools/SML/Examples.thy
--- 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>