# HG changeset patch
# User nipkow
# Date 1403433475 -7200
# Node ID 886ff14f20cc2d78a095d68635a2054dad6e9207
# Parent  1f133cd8d3eb71258c197b1ea7d1716f3956a468
r_into_(r)trancl should not be [simp]: helps little and comlicates some AFP proofs

diff -r 1f133cd8d3eb -r 886ff14f20cc src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Sat Jun 21 15:46:52 2014 +0200
+++ b/src/HOL/Transitive_Closure.thy	Sun Jun 22 12:37:55 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,simp]: "!!p. p \<in> r ==> p \<in> r^*"
+lemma r_into_rtrancl [intro]: "!!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'[simp]: "!!p. p : r ==> p : r^+"
+lemma r_into_trancl': "!!p. p : r ==> p : r^+"
   by (simp only: split_tupled_all) (erule r_into_trancl)
 
 text {*
diff -r 1f133cd8d3eb -r 886ff14f20cc src/HOL/UNITY/Comp/PriorityAux.thy
--- a/src/HOL/UNITY/Comp/PriorityAux.thy	Sat Jun 21 15:46:52 2014 +0200
+++ b/src/HOL/UNITY/Comp/PriorityAux.thy	Sun Jun 22 12:37:55 2014 +0200
@@ -95,7 +95,7 @@
 apply (erule ImageE)
 apply (erule trancl_induct) 
  apply (cases "i=k", simp_all) 
- apply (blast, clarify) 
+ apply (blast, 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)