# HG changeset patch
# User hoelzl
# Date 1287741672 -7200
# Node ID 0bee30e3a4ad67925564d55dabeb3b1223f75a3f
# Parent  1f7cc5357d96526b7a35b5cd0a7d8addf2c3d611
Changed section title to please LaTeX.

diff -r 1f7cc5357d96 -r 0bee30e3a4ad src/HOL/Lazy_Sequence.thy
--- a/src/HOL/Lazy_Sequence.thy	Thu Oct 21 20:26:35 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Fri Oct 22 12:01:12 2010 +0200
@@ -150,7 +150,7 @@
   "product s1 s2 = Lazy_Sequence.bind s1 (%a. Lazy_Sequence.bind s2 (%b. Lazy_Sequence.single (a, b)))"
 
 
-subsubsection {* small_lazy typeclasses *}
+subsubsection {* Small lazy typeclasses *}
 
 class small_lazy =
   fixes small_lazy :: "int \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"