src/HOL/Nitpick.thy
changeset 45140 339a8b3c4791
parent 44278 1220ecb81e8f
child 45970 b6d0cff57d96
     1.1 --- a/src/HOL/Nitpick.thy	Thu Oct 13 23:02:59 2011 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Thu Oct 13 23:27:46 2011 +0200
     1.3 @@ -63,7 +63,7 @@
     1.4  by (auto simp: mem_def)
     1.5  
     1.6  lemma rtrancl_unfold [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
     1.7 -by simp
     1.8 +  by (simp only: rtrancl_trancl_reflcl)
     1.9  
    1.10  lemma rtranclp_unfold [nitpick_unfold, no_atp]:
    1.11  "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)"