src/HOL/Set.thy
 changeset 3842 b55686a7b22c parent 3820 46b255e140dc child 3947 eb707467f8c5
```     1.1 --- a/src/HOL/Set.thy	Fri Oct 10 18:37:49 1997 +0200
1.2 +++ b/src/HOL/Set.thy	Fri Oct 10 19:02:28 1997 +0200
1.3 @@ -125,8 +125,8 @@
1.4
1.5    (* Isomorphisms between Predicates and Sets *)
1.6
1.7 -  mem_Collect_eq    "(a : {x.P(x)}) = P(a)"
1.8 -  Collect_mem_eq    "{x.x:A} = A"
1.9 +  mem_Collect_eq    "(a : {x. P(x)}) = P(a)"
1.10 +  Collect_mem_eq    "{x. x:A} = A"
1.11
1.12
1.13  defs
1.14 @@ -136,18 +136,18 @@
1.15    subset_def    "A <= B         == ! x:A. x:B"
1.16    psubset_def   "A < B          == (A::'a set) <= B & ~ A=B"
1.17    Compl_def     "Compl A        == {x. ~x:A}"
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 +  Un_def        "A Un B         == {x. x:A | x:B}"
1.21 +  Int_def       "A Int B        == {x. x:A & x:B}"
1.22    set_diff_def  "A - B          == {x. x:A & ~x:B}"
1.23    INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"
1.24    UNION_def     "UNION A B      == {y. ? x:A. y: B(x)}"
1.25 -  INTER1_def    "INTER1 B       == INTER {x.True} B"
1.26 -  UNION1_def    "UNION1 B       == UNION {x.True} B"
1.27 +  INTER1_def    "INTER1 B       == INTER {x. True} B"
1.28 +  UNION1_def    "UNION1 B       == UNION {x. True} B"
1.29    Inter_def     "Inter S        == (INT x:S. x)"
1.30    Union_def     "Union S        == (UN x:S. x)"
1.31    Pow_def       "Pow A          == {B. B <= A}"
1.32    empty_def     "{}             == {x. False}"
1.33 -  insert_def    "insert a B     == {x.x=a} Un B"
1.34 +  insert_def    "insert a B     == {x. x=a} Un B"
1.35    image_def     "f``A           == {y. ? x:A. y=f(x)}"
1.36
1.37  end
```