src/ZF/Resid/Redex.thy

--- a/src/ZF/Resid/Redex.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Resid/Redex.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -21,8 +21,8 @@
  
 defs
   redex_rec_def
-   "redex_rec(p,b,c,d) == \
-\   Vrec(p, %p g.redexes_case(b, %x.c(x,g`x),   \
-\                             %n x y.d(n, x, y, g`x, g`y), p))"
+   "redex_rec(p,b,c,d) == 
+   Vrec(p, %p g.redexes_case(b, %x.c(x,g`x),   
+                             %n x y.d(n, x, y, g`x, g`y), p))"
 end