undid split_comp_eq[simp] because it leads to nontermination together with split_def!

--- a/src/HOL/Product_Type.thy	Sat Jan 03 16:09:39 2004 +0100
+++ b/src/HOL/Product_Type.thy	Mon Jan 05 00:46:06 2004 +0100
@@ -484,7 +484,11 @@
   apply (rule ext, blast)
   done
 
-lemma split_comp_eq [simp]: 
+(* Do NOT make this a simp rule as it
+   a) only helps in special situations
+   b) can lead to nontermination in the presence of split_def
+*)
+lemma split_comp_eq: 
 "(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))"
 by (rule ext, auto)
 

--- a/src/HOL/Transitive_Closure.thy	Sat Jan 03 16:09:39 2004 +0100
+++ b/src/HOL/Transitive_Closure.thy	Mon Jan 05 00:46:06 2004 +0100
@@ -402,6 +402,16 @@
 text {* More about converse @{text rtrancl} and @{text trancl}, should
   be merged with main body. *}
 
+lemma single_valued_confluent:
+  "\<lbrakk> single_valued r; (x,y) \<in> r^*; (x,z) \<in> r^* \<rbrakk>
+  \<Longrightarrow> (y,z) \<in> r^* \<or> (z,y) \<in> r^*"
+apply(erule rtrancl_induct)
+ apply simp
+apply(erule disjE)
+ apply(blast elim:converse_rtranclE dest:single_valuedD)
+apply(blast intro:rtrancl_trans)
+done
+
 lemma r_r_into_trancl: "(a, b) \<in> R ==> (b, c) \<in> R ==> (a, c) \<in> R^+"
   by (fast intro: trancl_trans)