lemmas about proper subset relation;
authorwenzelm
Fri Apr 16 16:47:30 1999 +0200 (1999-04-16)
changeset 64436d5d3ecedf50
parent 6442 6a95ceaa977e
child 6444 2ebe9e630cab
lemmas about proper subset relation;
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Fri Apr 16 14:50:30 1999 +0200
     1.2 +++ b/src/HOL/Set.ML	Fri Apr 16 16:47:30 1999 +0200
     1.3 @@ -686,3 +686,13 @@
     1.4  qed "psubset_insertD";
     1.5  
     1.6  bind_thm ("psubset_eq", psubset_def RS meta_eq_to_obj_eq);
     1.7 +
     1.8 +bind_thm ("psubset_imp_subset", psubset_eq RS iffD1 RS conjunct1);
     1.9 +
    1.10 +Goal"[| (A::'a set) < B; B <= C |] ==> A < C";
    1.11 +by (auto_tac (claset(), simpset() addsimps [psubset_eq]));
    1.12 +qed "psubset_subset_trans";
    1.13 +
    1.14 +Goal"[| (A::'a set) <= B; B < C|] ==> A < C";
    1.15 +by (auto_tac (claset(), simpset() addsimps [psubset_eq]));
    1.16 +qed "subset_psubset_trans";