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