diff -r c3913a79b6ae -r 492493334e0f Univ.thy
--- a/Univ.thy	Fri Apr 14 11:23:33 1995 +0200
+++ b/Univ.thy	Wed Jun 21 15:12:40 1995 +0200
@@ -45,10 +45,10 @@
   Case   :: "[['a item]=>'b, ['a item]=>'b, 'a item] => 'b"
 
   diag   :: "'a set => ('a * 'a)set"
-  "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \
-\           => ('a item * 'a item)set" (infixr 80)
-  "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \
-\           => ('a item * 'a item)set" (infixr 70)
+  "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
+           => ('a item * 'a item)set" (infixr 80)
+  "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
+           => ('a item * 'a item)set" (infixr 70)
 
 defs
 
@@ -86,18 +86,18 @@
   (*the corresponding eliminators*)
   Split_def  "Split(c,M) == @u. ? x y. M = x$y & u = c(x,y)"
 
-  Case_def   "Case(c,d,M) == @u.  (? x . M = In0(x) & u = c(x)) \
-\                               | (? y . M = In1(y) & u = d(y))"
+  Case_def   "Case(c,d,M) == @u.  (? x . M = In0(x) & u = c(x)) 
+                               | (? y . M = In1(y) & u = d(y))"
 
 
   (** diagonal sets and equality for the "universe" **)
 
   diag_def   "diag(A) == UN x:A. {<x,x>}"
 
-  dprod_def  "r<**>s == UN u:r. split(%x x'. \
-\                       UN v:s. split(%y y'. {<x$y,x'$y'>}, v), u)"
+  dprod_def  "r<**>s == UN u:r. split(%x x'. 
+                       UN v:s. split(%y y'. {<x$y,x'$y'>}, v), u)"
 
-  dsum_def   "r<++>s == (UN u:r. split(%x x'. {<In0(x),In0(x')>}, u)) Un \
-\                       (UN v:s. split(%y y'. {<In1(y),In1(y')>}, v))"
+  dsum_def   "r<++>s == (UN u:r. split(%x x'. {<In0(x),In0(x')>}, u)) Un 
+                       (UN v:s. split(%y y'. {<In1(y),In1(y')>}, v))"
 
 end