src/HOL/Set.thy
changeset 13624 17684cf64fda
parent 13550 5a176b8dda84
child 13653 ef123b9e8089
     1.1 --- a/src/HOL/Set.thy	Thu Oct 03 09:54:54 2002 +0200
     1.2 +++ b/src/HOL/Set.thy	Thu Oct 03 10:34:51 2002 +0200
     1.3 @@ -834,6 +834,10 @@
     1.4  lemma psubsetI [intro!]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
     1.5    by (unfold psubset_def) blast
     1.6  
     1.7 +lemma psubsetE [elim!]: 
     1.8 +    "[|A \<subset> B;  [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
     1.9 +  by (unfold psubset_def) blast
    1.10 +
    1.11  lemma psubset_insert_iff:
    1.12    "(A \<subset> insert x B) = (if x \<in> B then A \<subset> B else if x \<in> A then A - {x} \<subset> B else A \<subseteq> B)"
    1.13    by (auto simp add: psubset_def subset_insert_iff)