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