# HG changeset patch
# User wenzelm
# Date 924274050 -7200
# Node ID 6d5d3ecedf50fb2003d8008047c86d7d3478b3c4
# Parent  6a95ceaa977ec6d0b0176a21d535e7df139f0e39
lemmas about proper subset relation;

diff -r 6a95ceaa977e -r 6d5d3ecedf50 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Apr 16 14:50:30 1999 +0200
+++ b/src/HOL/Set.ML	Fri Apr 16 16:47:30 1999 +0200
@@ -686,3 +686,13 @@
 qed "psubset_insertD";
 
 bind_thm ("psubset_eq", psubset_def RS meta_eq_to_obj_eq);
+
+bind_thm ("psubset_imp_subset", psubset_eq RS iffD1 RS conjunct1);
+
+Goal"[| (A::'a set) < B; B <= C |] ==> A < C";
+by (auto_tac (claset(), simpset() addsimps [psubset_eq]));
+qed "psubset_subset_trans";
+
+Goal"[| (A::'a set) <= B; B < C|] ==> A < C";
+by (auto_tac (claset(), simpset() addsimps [psubset_eq]));
+qed "subset_psubset_trans";