src/HOL/Set.thy
changeset 3222 726a9b069947
parent 2965 afbda7e26f15
child 3370 5c5fdce3a4e4
     1.1 --- a/src/HOL/Set.thy	Fri May 16 17:14:55 1997 +0200
     1.2 +++ b/src/HOL/Set.thy	Fri May 16 17:40:41 1997 +0200
     1.3 @@ -133,6 +133,7 @@
     1.4    Ball_def      "Ball A P       == ! x. x:A --> P(x)"
     1.5    Bex_def       "Bex A P        == ? x. x:A & P(x)"
     1.6    subset_def    "A <= B         == ! x:A. x:B"
     1.7 +  psubset_def   "A < B          == (A::'a set) <= B & ~ A=B"
     1.8    Compl_def     "Compl A        == {x. ~x:A}"
     1.9    Un_def        "A Un B         == {x.x:A | x:B}"
    1.10    Int_def       "A Int B        == {x.x:A & x:B}"