# HG changeset patch
# User nipkow
# Date 1403358412 -7200
# Node ID 1f133cd8d3eb71258c197b1ea7d1716f3956a468
# Parent  7da3e398804c2412e832c99193fd19e0909da7f6
added [simp]

diff -r 7da3e398804c -r 1f133cd8d3eb src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Sat Jun 21 10:41:02 2014 +0200
+++ b/src/HOL/Transitive_Closure.thy	Sat Jun 21 15:46:52 2014 +0200
@@ -87,7 +87,7 @@
 lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r \<union> Id)"
   by (auto simp add: fun_eq_iff)
 
-lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
+lemma r_into_rtrancl [intro,simp]: "!!p. p \<in> r ==> p \<in> r^*"
   -- {* @{text rtrancl} of @{text r} contains @{text r} *}
   apply (simp only: split_tupled_all)
   apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl])
@@ -340,7 +340,7 @@
    apply (iprover dest: subsetD)+
   done
 
-lemma r_into_trancl': "!!p. p : r ==> p : r^+"
+lemma r_into_trancl'[simp]: "!!p. p : r ==> p : r^+"
   by (simp only: split_tupled_all) (erule r_into_trancl)
 
 text {*
diff -r 7da3e398804c -r 1f133cd8d3eb src/HOL/UNITY/Comp/PriorityAux.thy
--- a/src/HOL/UNITY/Comp/PriorityAux.thy	Sat Jun 21 10:41:02 2014 +0200
+++ b/src/HOL/UNITY/Comp/PriorityAux.thy	Sat Jun 21 15:46:52 2014 +0200
@@ -95,7 +95,7 @@
 apply (erule ImageE)
 apply (erule trancl_induct) 
  apply (cases "i=k", simp_all) 
-  apply (blast, blast, clarify) 
+ apply (blast, clarify) 
 apply (drule_tac x = y in spec)
 apply (drule_tac x = z in spec)
 apply (blast dest: r_into_trancl intro: trancl_trans)