src/ZF/Sum.thy
changeset 38514 bd9c4e8281ec
parent 35416 d8d7d1b785af
child 41777 1f7cbe39d425
     1.1 --- a/src/ZF/Sum.thy	Wed Aug 18 12:08:21 2010 +0200
     1.2 +++ b/src/ZF/Sum.thy	Wed Aug 18 12:19:27 2010 +0200
     1.3 @@ -9,8 +9,6 @@
     1.4  
     1.5  text{*And the "Part" primitive for simultaneous recursive type definitions*}
     1.6  
     1.7 -global
     1.8 -
     1.9  definition sum :: "[i,i]=>i" (infixr "+" 65) where
    1.10       "A+B == {0}*A Un {1}*B"
    1.11  
    1.12 @@ -27,8 +25,6 @@
    1.13  definition Part :: "[i,i=>i] => i" where
    1.14       "Part(A,h) == {x: A. EX z. x = h(z)}"
    1.15  
    1.16 -local
    1.17 -
    1.18  subsection{*Rules for the @{term Part} Primitive*}
    1.19  
    1.20  lemma Part_iff: