# HG changeset patch
# User lcp
# Date 777545805 -7200
# Node ID 6927e1cb2c071987f3b2716a10d5ed985c614173
# Parent  2536dfe47b75f0c590d0dd31c48fb40c01dfaf3b
HOL/Sum.thy: generalized the type of Part

diff -r 2536dfe47b75 -r 6927e1cb2c07 Sum.thy
--- 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)"