src/ZF/Sum.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 2469 b50b8c0eec01
     1.1 --- a/src/ZF/Sum.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/Sum.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	ZF/sum.thy
     1.5 +(*  Title:      ZF/sum.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1993  University of Cambridge
    1.10  
    1.11  Disjoint sums in Zermelo-Fraenkel Set Theory 
    1.12 @@ -9,7 +9,7 @@
    1.13  
    1.14  Sum = Bool + "simpdata" +
    1.15  consts
    1.16 -    "+"    	:: [i,i]=>i      		(infixr 65)
    1.17 +    "+"         :: [i,i]=>i                     (infixr 65)
    1.18      Inl,Inr     :: i=>i
    1.19      case        :: [i=>i, i=>i, i]=>i
    1.20      Part        :: [i,i=>i] => i
    1.21 @@ -21,5 +21,5 @@
    1.22      case_def    "case(c,d) == (%<y,z>. cond(y, d(z), c(z)))"
    1.23  
    1.24    (*operator for selecting out the various summands*)
    1.25 -    Part_def	"Part(A,h) == {x: A. EX z. x = h(z)}"
    1.26 +    Part_def    "Part(A,h) == {x: A. EX z. x = h(z)}"
    1.27  end