# HG changeset patch
# User webertj
# Date 1274616001 -3600
# Node ID 088ad0b57137cd6956ceca3b4fd26f8fb346d0e4
# Parent  f1a07303d9925d2f3120d41b089ba4abe84986b0
Improved document structure.

diff -r f1a07303d992 -r 088ad0b57137 src/HOL/Library/Kleene_Algebra.thy
--- a/src/HOL/Library/Kleene_Algebra.thy	Sun May 23 10:55:01 2010 +0100
+++ b/src/HOL/Library/Kleene_Algebra.thy	Sun May 23 13:00:01 2010 +0100
@@ -3,7 +3,7 @@
     Author:     Tjark Weber, University of Cambridge
 *)
 
-header {* Kleene Algebra *}
+header {* Kleene Algebras *}
 
 theory Kleene_Algebra
 imports Main 
@@ -124,7 +124,7 @@
 
 end
 
-section {* Kleene Algebras *}
+subsection {* A class of Kleene algebras *}
 
 text {* Class @{text pre_kleene} provides all operations of Kleene
   algebras except for the Kleene star. *}
@@ -352,7 +352,7 @@
 
 end
 
-subsection {* Complete Lattices are Kleene Algebras *}
+subsection {* Complete lattices are Kleene algebras *}
 
 lemma (in complete_lattice) le_SUPI':
   assumes "l \<le> M i"
@@ -458,7 +458,7 @@
 
 end
 
-subsection {* Transitive Closure *}
+subsection {* Transitive closure *}
 
 context kleene
 begin
@@ -477,7 +477,7 @@
 
 end
 
-subsection {* A Naive Algorithm to Generate the Transitive Closure *}
+subsection {* A naive algorithm to generate the transitive closure *}
 
 function (default "\<lambda>x. 0", tailrec, domintros)
   mk_tcl :: "('a::{plus,times,ord,zero}) \<Rightarrow> 'a \<Rightarrow> 'a"