--- a/src/ZF/ex/LListFn.thy Sat Apr 05 16:18:58 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(* Title: ZF/ex/llist-fn.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Functions for Lazy Lists in Zermelo-Fraenkel Set Theory
-
-STILL NEEDS:
-co_recursion for defining lconst, flip, etc.
-a typing rule for it, based on some notion of "productivity..."
-*)
-
-LListFn = LList + LList_Eq +
-consts
- lconst :: "i => i"
- flip :: "i => i"
-
-rules
- lconst_def "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
-
- flip_LNil "flip(LNil) = LNil"
-
- flip_LCons "[| x:bool; l: llist(bool) |] ==> \
-\ flip(LCons(x,l)) = LCons(not(x), flip(l))"
-
-end