--- a/src/HOL/HoareParallel/RG_Examples.thy Sat May 04 15:47:21 2002 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy Mon May 06 09:42:20 2002 +0200
@@ -1,4 +1,3 @@
-
header {* \section{Examples} *}
theory RG_Examples = RG_Syntax:
@@ -340,12 +339,7 @@
apply simp+
apply(erule_tac x=j in allE)
apply force
- apply simp
- apply clarify
- apply(rule conjI)
- apply clarify
- apply simp
- apply(erule not_sym)
+ apply clarsimp
apply force
apply force+
done
--- a/src/HOL/Set.thy Sat May 04 15:47:21 2002 +0200
+++ b/src/HOL/Set.thy Mon May 06 09:42:20 2002 +0200
@@ -1049,6 +1049,13 @@
lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
by blast
+lemma insert_disjoint[simp]:
+ "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
+by blast
+
+lemma disjoint_insert[simp]:
+ "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
+by blast
text {* \medskip @{text image}. *}