src/ZF/ex/LListFn.thy

--- a/src/ZF/ex/LListFn.thy	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/ex/LListFn.thy	Mon Nov 15 14:41:25 1993 +0100
@@ -4,13 +4,23 @@
     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 +
+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