--- 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";