src/ZF/Sum.thy
changeset 32960 69916a850301
parent 24893 b8ef7afe3a6b
child 35416 d8d7d1b785af
     1.1 --- a/src/ZF/Sum.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/ZF/Sum.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -1,8 +1,6 @@
     1.4  (*  Title:      ZF/sum.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   1993  University of Cambridge
     1.8 -
     1.9  *)
    1.10  
    1.11  header{*Disjoint Sums*}
    1.12 @@ -161,8 +159,7 @@
    1.13  by auto 
    1.14  
    1.15  lemma case_case: "z: A+B ==>    
    1.16 -        
    1.17 -	case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) =  
    1.18 +        case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) =  
    1.19          case(%x. c(c'(x)), %y. d(d'(y)), z)"
    1.20  by auto
    1.21