src/ZF/ex/LList.thy
changeset 1155 928a16e02f9f
parent 810 91c68f74f458
child 1401 0c439768f45c
--- a/src/ZF/ex/LList.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/LList.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -49,8 +49,8 @@
 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