--- 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 {*
--- 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 {*
--- 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 =