src/HOL/Induct/LFilter.thy

--- a/src/HOL/Induct/LFilter.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Induct/LFilter.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
 header {*The "filter" functional for coinductive lists
   --defined by a combination of induction and coinduction*}
 
-theory LFilter = LList:
+theory LFilter imports LList begin
 
 consts
   findRel	:: "('a => bool) => ('a llist * 'a llist)set"