diff -r bdcaa3f3a2f4 -r 339a8b3c4791 src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Thu Oct 13 23:02:59 2011 +0200 +++ b/src/HOL/Nitpick.thy Thu Oct 13 23:27:46 2011 +0200 @@ -63,7 +63,7 @@ by (auto simp: mem_def) lemma rtrancl_unfold [nitpick_unfold, no_atp]: "r\<^sup>* \ (r\<^sup>+)\<^sup>=" -by simp + by (simp only: rtrancl_trancl_reflcl) lemma rtranclp_unfold [nitpick_unfold, no_atp]: "rtranclp r a b \ (a = b \ tranclp r a b)"