diff -r 7c6476c53a6c -r 361521bc7c47 Univ.thy
--- a/Univ.thy	Thu Aug 18 12:13:26 1994 +0200
+++ b/Univ.thy	Thu Aug 18 12:23:52 1994 +0200
@@ -11,7 +11,7 @@
 Could <*> be generalized to a general summation (Sigma)?
 *)
 
-Univ = Arith +
+Univ = Arith + Sum + 
 
 types
   'a node
@@ -42,8 +42,8 @@
   "<*>"  :: "['a node set set, 'a node set set]=> 'a node set set" (infixr 80)
   "<+>"  :: "['a node set set, 'a node set set]=> 'a node set set" (infixr 70)
 
-  Split	 :: "['a node set, ['a node set, 'a node set]=>'b] => 'b"
-  Case   :: "['a node set, ['a node set]=>'b, ['a node set]=>'b] => 'b"
+  Split	 :: "[['a node set, 'a node set]=>'b, 'a node set] => 'b"
+  Case   :: "[['a node set]=>'b, ['a node set]=>'b, 'a node set] => 'b"
 
   diag   :: "'a set => ('a * 'a)set"
   "<**>" :: "[('a node set * 'a node set)set, ('a node set * 'a node set)set] \
@@ -65,8 +65,8 @@
   Push_Node_def    "Push_Node == (%n x. Abs_Node (apfst(Push(n),Rep_Node(x))))"
 
   (*crude "lists" of nats -- needed for the constructions*)
-  apfst_def  "apfst == (%f p.split(p, %x y. <f(x),y>))"
-  Push_def   "Push == (%b h n. nat_case(n,Suc(b),h))"
+  apfst_def  "apfst == (%f. split(%x y. <f(x),y>))"
+  Push_def   "Push == (%b h. nat_case(Suc(b),h))"
 
   (** operations on S-expressions -- sets of nodes **)
 
@@ -83,7 +83,7 @@
   In1_def    "In1(M) == Numb(Suc(0)) $ M"
 
   (*the set of nodes with depth less than k*)
-  ndepth_def "ndepth(n) == split(Rep_Node(n), %f x. LEAST k. f(k)=0)"
+  ndepth_def "ndepth(n) == split(%f x. LEAST k. f(k)=0, Rep_Node(n))"
   ntrunc_def "ntrunc(k,N) == {n. n:N & ndepth(n)<k}"
 
   (*products and sums for the "universe"*)
@@ -91,9 +91,9 @@
   usum_def   "A<+>B == In0``A Un In1``B"
 
   (*the corresponding eliminators*)
-  Split_def  "Split(M,c) == @u. ? x y. M = x$y & u = c(x,y)"
+  Split_def  "Split(c,M) == @u. ? x y. M = x$y & u = c(x,y)"
 
-  Case_def   "Case(M,c,d) == @u.  (? x . M = In0(x) & u = c(x))	\
+  Case_def   "Case(c,d,M) == @u.  (? x . M = In0(x) & u = c(x))	\
 \	   	                | (? y . M = In1(y) & u = d(y))"
 
 
@@ -101,10 +101,10 @@
 
   diag_def   "diag(A) == UN x:A. {<x,x>}"
 
-  dprod_def  "r<**>s == UN u:r. UN v:s. \
-\                       split(u, %x x'. split(v, %y y'. {<x$y,x'$y'>}))"
+  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(u, %x x'. {<In0(x),In0(x')>})) Un \
-\                       (UN v:s. split(v, %y y'. {<In1(y),In1(y')>}))"
+  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