| changeset 40056 | 0bee30e3a4ad |
| parent 40051 | b6acda4d1c29 |
| child 42163 | 392fd6c4669c |
--- 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"