# HG changeset patch
# User haftmann
# Date 1166021129 -3600
# Node ID 4d2ad5445c8183810374a87e61c58ad4b437407d
# Parent  0210a5db2013040cb8c4ddc89a6eb9943e740185
dropped superfluous header

diff -r 0210a5db2013 -r 4d2ad5445c81 src/HOL/Library/MLString.thy
--- a/src/HOL/Library/MLString.thy	Wed Dec 13 14:56:50 2006 +0100
+++ b/src/HOL/Library/MLString.thy	Wed Dec 13 15:45:29 2006 +0100
@@ -8,8 +8,6 @@
 imports List
 begin
 
-section {* Monolithic strings for ML *}
-
 subsection {* Motivation *}
 
 text {*
diff -r 0210a5db2013 -r 4d2ad5445c81 src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Wed Dec 13 14:56:50 2006 +0100
+++ b/src/HOL/Library/State_Monad.thy	Wed Dec 13 15:45:29 2006 +0100
@@ -9,8 +9,6 @@
 imports Main
 begin
 
-section {* Generic, open state monads *}
-
 subsection {* Motivation *}
 
 text {*
diff -r 0210a5db2013 -r 4d2ad5445c81 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Dec 13 14:56:50 2006 +0100
+++ b/src/HOL/Orderings.thy	Wed Dec 13 15:45:29 2006 +0100
@@ -9,8 +9,6 @@
 imports HOL
 begin
 
-section {* Abstract orders *}
-
 subsection {* Order syntax *}
 
 class ord =