1.1 --- a/src/HOL/Set.ML	Fri Nov 05 12:47:15 1999 +0100
     1.2 +++ b/src/HOL/Set.ML	Fri Nov 05 12:47:29 1999 +0100
     1.3 @@ -727,7 +727,7 @@
     1.4  Addsimps[subset_UNIV, subset_refl];
     1.5  
     1.6  
     1.7 -(*** < ***)
     1.8 +(*** The 'proper subset' relation (<) ***)
     1.9  
    1.10  Goalw [psubset_def] "!!A::'a set. [| A <= B; A ~= B |] ==> A<B";
    1.11  by (Blast_tac 1);
    1.12 @@ -750,6 +750,10 @@
    1.13  by (auto_tac (claset(), simpset() addsimps [psubset_eq]));
    1.14  qed "subset_psubset_trans";
    1.15  
    1.16 +Goalw [psubset_def] "A < B ==> EX b. b : (B - A)";
    1.17 +by (Blast_tac 1);
    1.18 +qed "psubset_imp_ex_mem";
    1.19 +
    1.20  
    1.21  (* attributes *)
    1.22