src/HOL/Set.thy
changeset 3222 726a9b069947
parent 2965 afbda7e26f15
child 3370 5c5fdce3a4e4
equal deleted inserted replaced
3221:90211fa9ee7e 3222:726a9b069947
   131 defs
   131 defs
   132 
   132 
   133   Ball_def      "Ball A P       == ! x. x:A --> P(x)"
   133   Ball_def      "Ball A P       == ! x. x:A --> P(x)"
   134   Bex_def       "Bex A P        == ? x. x:A & P(x)"
   134   Bex_def       "Bex A P        == ? x. x:A & P(x)"
   135   subset_def    "A <= B         == ! x:A. x:B"
   135   subset_def    "A <= B         == ! x:A. x:B"
       
   136   psubset_def   "A < B          == (A::'a set) <= B & ~ A=B"
   136   Compl_def     "Compl A        == {x. ~x:A}"
   137   Compl_def     "Compl A        == {x. ~x:A}"
   137   Un_def        "A Un B         == {x.x:A | x:B}"
   138   Un_def        "A Un B         == {x.x:A | x:B}"
   138   Int_def       "A Int B        == {x.x:A & x:B}"
   139   Int_def       "A Int B        == {x.x:A & x:B}"
   139   set_diff_def  "A - B          == {x. x:A & ~x:B}"
   140   set_diff_def  "A - B          == {x. x:A & ~x:B}"
   140   INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"
   141   INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"