Sum.thy
changeset 122 6927e1cb2c07
parent 117 3716c99fb6a1
child 128 89669c58e506
--- a/Sum.thy	Fri Aug 19 16:18:44 1994 +0200
+++ b/Sum.thy	Mon Aug 22 10:56:45 1994 +0200
@@ -26,7 +26,7 @@
 
   (*disjoint sum for sets; the operator + is overloaded with wrong type!*)
   "plus"   :: "['a set, 'b set] => ('a+'b)set"      	(infixr 65)
-  Part     :: "['a set, 'a=>'a] => 'a set"
+  Part     :: "['a set, 'b=>'a] => 'a set"
 
 translations
   "case p of Inl(x) => a | Inr(y) => b" == "sum_case(%x.a, %y.b, p)"