src/CCL/Set.thy
changeset 3837 d7f033c74b38
parent 278 523518f44286
child 3935 52c14fe8f16b
     1.1 --- a/src/CCL/Set.thy	Fri Oct 10 16:29:41 1997 +0200
     1.2 +++ b/src/CCL/Set.thy	Fri Oct 10 17:10:12 1997 +0200
     1.3 @@ -50,17 +50,17 @@
     1.4  
     1.5  
     1.6  rules
     1.7 -  mem_Collect_iff       "(a : {x.P(x)}) <-> P(a)"
     1.8 -  set_extension         "A=B <-> (ALL x.x:A <-> x:B)"
     1.9 +  mem_Collect_iff       "(a : {x. P(x)}) <-> P(a)"
    1.10 +  set_extension         "A=B <-> (ALL x. x:A <-> x:B)"
    1.11  
    1.12    Ball_def      "Ball(A, P)  == ALL x. x:A --> P(x)"
    1.13    Bex_def       "Bex(A, P)   == EX x. x:A & P(x)"
    1.14    mono_def      "mono(f)     == (ALL A B. A <= B --> f(A) <= f(B))"
    1.15    subset_def    "A <= B      == ALL x:A. x:B"
    1.16 -  singleton_def "{a}         == {x.x=a}"
    1.17 -  empty_def     "{}          == {x.False}"
    1.18 -  Un_def        "A Un B      == {x.x:A | x:B}"
    1.19 -  Int_def       "A Int B     == {x.x:A & x:B}"
    1.20 +  singleton_def "{a}         == {x. x=a}"
    1.21 +  empty_def     "{}          == {x. False}"
    1.22 +  Un_def        "A Un B      == {x. x:A | x:B}"
    1.23 +  Int_def       "A Int B     == {x. x:A & x:B}"
    1.24    Compl_def     "Compl(A)    == {x. ~x:A}"
    1.25    INTER_def     "INTER(A, B) == {y. ALL x:A. y: B(x)}"
    1.26    UNION_def     "UNION(A, B) == {y. EX x:A. y: B(x)}"