changeset 25595 | 6c48275f9c76 |
parent 24863 | 307b979b1f54 |
child 27368 | 9f90ac19e32b |
--- a/src/HOL/Library/Coinductive_List.thy Mon Dec 10 11:24:09 2007 +0100 +++ b/src/HOL/Library/Coinductive_List.thy Mon Dec 10 11:24:12 2007 +0100 @@ -6,7 +6,7 @@ header {* Potentially infinite lists as greatest fixed-point *} theory Coinductive_List -imports Main +imports List begin subsection {* List constructors over the datatype universe *}