equal
deleted
inserted
replaced
61 apply (rename_tac y) |
61 apply (rename_tac y) |
62 apply (erule_tac x = y in allE) |
62 apply (erule_tac x = y in allE) |
63 by (auto simp: mem_def) |
63 by (auto simp: mem_def) |
64 |
64 |
65 lemma rtrancl_unfold [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>=" |
65 lemma rtrancl_unfold [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>=" |
66 by simp |
66 by (simp only: rtrancl_trancl_reflcl) |
67 |
67 |
68 lemma rtranclp_unfold [nitpick_unfold, no_atp]: |
68 lemma rtranclp_unfold [nitpick_unfold, no_atp]: |
69 "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)" |
69 "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)" |
70 by (rule eq_reflection) (auto dest: rtranclpD) |
70 by (rule eq_reflection) (auto dest: rtranclpD) |
71 |
71 |