--- a/src/HOL/ex/LFilter.thy Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(* Title: HOL/LList.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-
-The "filter" functional for coinductive lists
- --defined by a combination of induction and coinduction
-*)
-
-LFilter = LList + Relation +
-
-consts
- findRel :: "('a => bool) => ('a llist * 'a llist)set"
-
-inductive "findRel p"
- intrs
- found "p x ==> (LCons x l, LCons x l) : findRel p"
- seek "[| ~p x; (l,l') : findRel p |] ==> (LCons x l, l') : findRel p"
-
-constdefs
- find :: ['a => bool, 'a llist] => 'a llist
- "find p l == @l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p))"
-
- lfilter :: ['a => bool, 'a llist] => 'a llist
- "lfilter p l == llist_corec l (%l. case find p l of
- LNil => Inl ()
- | LCons y z => Inr(y,z))"
-
-end