src/ZF/ex/LList.thy

--- a/src/ZF/ex/LList.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/LList.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -43,9 +43,10 @@
   lconst   :: "i => i"
   flip     :: "i => i"
 
-rules
+defs
   lconst_def  "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
 
+rules
   flip_LNil   "flip(LNil) = LNil"
 
   flip_LCons  "[| x:bool; l: llist(bool) |] ==> \