# HG changeset patch
# User paulson
# Date 1033634091 -7200
# Node ID 17684cf64fdacf224453e9549b418fdd0bf57ad8
# Parent  c2b235e60f8bf76c78f08217f165bd6d50bbd871
added the new elim rule psubsetE

diff -r c2b235e60f8b -r 17684cf64fda src/HOL/HoareParallel/Gar_Coll.thy
--- a/src/HOL/HoareParallel/Gar_Coll.thy	Thu Oct 03 09:54:54 2002 +0200
+++ b/src/HOL/HoareParallel/Gar_Coll.thy	Thu Oct 03 10:34:51 2002 +0200
@@ -3,6 +3,8 @@
 
 theory Gar_Coll = Graph + OG_Syntax:
 
+declare psubsetE [rule del]
+
 text {* Declaration of variables: *}
 
 record gar_coll_state =
diff -r c2b235e60f8b -r 17684cf64fda src/HOL/Real/PReal.ML
--- a/src/HOL/Real/PReal.ML	Thu Oct 03 09:54:54 2002 +0200
+++ b/src/HOL/Real/PReal.ML	Thu Oct 03 10:34:51 2002 +0200
@@ -1167,14 +1167,7 @@
 \         ==> (ALL Y. (EX X: P. Y < X) = (Y < psup P))";              
 by (forward_tac [preal_sup RS Abs_preal_inverse] 1);
 by (Fast_tac 1);
-by (auto_tac (claset() addSIs [psubsetI],simpset() addsimps [psup_def,preal_less_def]));
-by (blast_tac (claset() addDs [psubset_def RS meta_eq_to_obj_eq RS iffD1]) 1);
-by (rotate_tac 4 1);
-by (asm_full_simp_tac (simpset() addsimps [psubset_def]) 1);
-by (dtac bspec 1 THEN assume_tac 1);
-by (REPEAT(etac conjE 1));
-by (EVERY1[rtac contrapos_np, assume_tac]);
-by (auto_tac (claset() addSDs [lemma_psubset_mem],simpset()));
+by (auto_tac (claset(), simpset() addsimps [psup_def,preal_less_def]));
 by (cut_inst_tac [("r1.0","Xa"),("r2.0","Ya")] preal_linear 1);
 by (auto_tac (claset() addDs [psubsetD],simpset() addsimps [preal_less_def]));
 qed "preal_complete";
diff -r c2b235e60f8b -r 17684cf64fda src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Oct 03 09:54:54 2002 +0200
+++ b/src/HOL/Set.thy	Thu Oct 03 10:34:51 2002 +0200
@@ -834,6 +834,10 @@
 lemma psubsetI [intro!]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
   by (unfold psubset_def) blast
 
+lemma psubsetE [elim!]: 
+    "[|A \<subset> B;  [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
+  by (unfold psubset_def) blast
+
 lemma psubset_insert_iff:
   "(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)"
   by (auto simp add: psubset_def subset_insert_iff)