Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Set.thy
changeset 3222 726a9b069947
parent 2965 afbda7e26f15
child 3370 5c5fdce3a4e4 
--- a/src/HOL/Set.thy	Fri May 16 17:14:55 1997 +0200
+++ b/src/HOL/Set.thy	Fri May 16 17:40:41 1997 +0200
@@ -133,6 +133,7 @@
   Ball_def      "Ball A P       == ! x. x:A --> P(x)"
   Bex_def       "Bex A P        == ? x. x:A & P(x)"
   subset_def    "A <= B         == ! x:A. x:B"
+  psubset_def   "A < B          == (A::'a set) <= B & ~ A=B"
   Compl_def     "Compl A        == {x. ~x:A}"
   Un_def        "A Un B         == {x.x:A | x:B}"
   Int_def       "A Int B        == {x.x:A & x:B}"
isabelle