src/ZF/ex/Integ.thy

--- a/src/ZF/ex/Integ.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/Integ.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -23,8 +23,8 @@
 defs
 
     intrel_def
-     "intrel == {p:(nat*nat)*(nat*nat). 		\
-\        EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
+     "intrel == {p:(nat*nat)*(nat*nat). 		
+        EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
 
     integ_def   "integ == (nat*nat)/intrel"
     
@@ -42,17 +42,17 @@
       Perhaps a "curried" or even polymorphic congruent predicate would be
       better.*)
     zadd_def
-     "Z1 $+ Z2 == \
-\       UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2                 \
-\                           in intrel``{<x1#+x2, y1#+y2>}"
+     "Z1 $+ Z2 == 
+       UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2                 
+                           in intrel``{<x1#+x2, y1#+y2>}"
     
     zdiff_def   "Z1 $- Z2 == Z1 $+ zminus(Z2)"
     zless_def	"Z1 $< Z2 == znegative(Z1 $- Z2)"
     
     (*This illustrates the primitive form of definitions (no patterns)*)
     zmult_def
-     "Z1 $* Z2 == \
-\       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2.        \
-\                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
+     "Z1 $* Z2 == 
+       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2.        
+                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
     
  end