src/HOL/Sum.thy
changeset 1423 5726a8243d3f
parent 1370 7361ac9b024d
child 1475 7f5a4cd08209
     1.1 --- a/src/HOL/Sum.thy	Sat Dec 23 12:50:53 1995 +0100
     1.2 +++ b/src/HOL/Sum.thy	Thu Dec 28 11:54:15 1995 +0100
     1.3 @@ -41,7 +41,7 @@
     1.4    Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
     1.5    Inr_def       "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
     1.6    sum_case_def  "sum_case f g p == @z.  (!x. p=Inl(x) --> z=f(x))      
     1.7 -                                     & (!y. p=Inr(y) --> z=g(y))"
     1.8 +                                      & (!y. p=Inr(y) --> z=g(y))"
     1.9  
    1.10    sum_def       "A plus B == (Inl``A) Un (Inr``B)"
    1.11