
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 {*




