| changeset 45140 | 339a8b3c4791 |
| parent 44278 | 1220ecb81e8f |
| child 45970 | b6d0cff57d96 |
--- 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>* \<equiv> (r\<^sup>+)\<^sup>=" -by simp + by (simp only: rtrancl_trancl_reflcl) lemma rtranclp_unfold [nitpick_unfold, no_atp]: "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)"