--- a/src/HOL/Set.ML Fri Nov 05 12:47:15 1999 +0100
+++ b/src/HOL/Set.ML Fri Nov 05 12:47:29 1999 +0100
@@ -727,7 +727,7 @@
Addsimps[subset_UNIV, subset_refl];
-(*** < ***)
+(*** The 'proper subset' relation (<) ***)
Goalw [psubset_def] "!!A::'a set. [| A <= B; A ~= B |] ==> A<B";
by (Blast_tac 1);
@@ -750,6 +750,10 @@
by (auto_tac (claset(), simpset() addsimps [psubset_eq]));
qed "subset_psubset_trans";
+Goalw [psubset_def] "A < B ==> EX b. b : (B - A)";
+by (Blast_tac 1);
+qed "psubset_imp_ex_mem";
+
(* attributes *)