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)}"
```