author | hoelzl |
Fri, 22 Oct 2010 12:01:12 +0200 | |
changeset 40056 | 0bee30e3a4ad |
parent 40055 | 1f7cc5357d96 |
child 40057 | b237f757b215 |
--- 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"