src/HOL/Set.thy
changeset 2393 651fce76c86c
parent 2388 d1f0505fc602
child 2412 025e80ed698d
     1.1 --- a/src/HOL/Set.thy	Fri Dec 13 18:32:07 1996 +0100
     1.2 +++ b/src/HOL/Set.thy	Fri Dec 13 18:40:50 1996 +0100
     1.3 @@ -127,24 +127,23 @@
     1.4    Ball_def      "Ball A P       == ! x. x:A --> P(x)"
     1.5    Bex_def       "Bex A P        == ? x. x:A & P(x)"
     1.6    subset_def    "A <= B         == ! x:A. x:B"
     1.7 -  Compl_def     "Compl(A)       == {x. ~x:A}"
     1.8 +  Compl_def     "Compl A        == {x. ~x:A}"
     1.9    Un_def        "A Un B         == {x.x:A | x:B}"
    1.10    Int_def       "A Int B        == {x.x:A & x:B}"
    1.11    set_diff_def  "A - B          == {x. x:A & ~x:B}"
    1.12    INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"
    1.13    UNION_def     "UNION A B      == {y. ? x:A. y: B(x)}"
    1.14 -  INTER1_def    "INTER1(B)      == INTER {x.True} B"
    1.15 -  UNION1_def    "UNION1(B)      == UNION {x.True} B"
    1.16 -  Inter_def     "Inter(S)       == (INT x:S. x)"
    1.17 -  Union_def     "Union(S)       == (UN x:S. x)"
    1.18 -  Pow_def       "Pow(A)         == {B. B <= A}"
    1.19 +  INTER1_def    "INTER1 B       == INTER {x.True} B"
    1.20 +  UNION1_def    "UNION1 B       == UNION {x.True} B"
    1.21 +  Inter_def     "Inter S        == (INT x:S. x)"
    1.22 +  Union_def     "Union S        == (UN x:S. x)"
    1.23 +  Pow_def       "Pow A          == {B. B <= A}"
    1.24    empty_def     "{}             == {x. False}"
    1.25    insert_def    "insert a B     == {x.x=a} Un B"
    1.26    image_def     "f``A           == {y. ? x:A. y=f(x)}"
    1.27 -  inj_def       "inj(f)         == ! x y. f(x)=f(y) --> x=y"
    1.28 +  inj_def       "inj f          == ! x y. f(x)=f(y) --> x=y"
    1.29    inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    1.30 -  surj_def      "surj(f)        == ! y. ? x. y=f(x)"
    1.31 -
    1.32 +  surj_def      "surj f         == ! y. ? x. y=f(x)"
    1.33  
    1.34  end
    1.35