src/ZF/ex/LList.thy

   lconst_def  "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
 
 rules
   flip_LNil   "flip(LNil) = LNil"
 
-  flip_LCons  "[| x:bool; l: llist(bool) |] ==> \
-\              flip(LCons(x,l)) = LCons(not(x), flip(l))"
+  flip_LCons  "[| x:bool; l: llist(bool) |] ==> 
+              flip(LCons(x,l)) = LCons(not(x), flip(l))"
 
 end