1.1 --- a/src/HOL/Set.ML	Fri May 16 17:14:55 1997 +0200
     1.2 +++ b/src/HOL/Set.ML	Fri May 16 17:40:41 1997 +0200
     1.3 @@ -666,3 +666,17 @@
     1.4  
     1.5  simpset := !simpset addcongs [ball_cong,bex_cong]
     1.6                      setmksimps (mksimps mksimps_pairs);
     1.7 +
     1.8 +Addsimps[subset_UNIV, empty_subsetI, subset_refl];
     1.9 +
    1.10 +
    1.11 +(*** < ***)
    1.12 +
    1.13 +goalw Set.thy [psubset_def] "!!A::'a set. [| A <= B; A ~= B |] ==> A<B";
    1.14 +by (Blast_tac 1);
    1.15 +qed "psubsetI";
    1.16 +
    1.17 +goalw Set.thy [psubset_def]
    1.18 +    "!!x. A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B";
    1.19 +by (Auto_tac());
    1.20 +qed "psubset_insertD";