changeset 67613 | ce654b0e6d69 |
parent 67399 | eab6ce8368fa |
child 67723 | d11c5af083a5 |
--- a/src/HOL/Transitive_Closure.thy Tue Feb 13 14:24:50 2018 +0100 +++ b/src/HOL/Transitive_Closure.thy Thu Feb 15 12:11:00 2018 +0100 @@ -243,7 +243,7 @@ lemmas rtrancl_converseI = rtranclp_converseI [to_set] -lemma rtrancl_converse: "(r^-1)\<^sup>* = (r\<^sup>*)^-1" +lemma rtrancl_converse: "(r\<inverse>)\<^sup>* = (r\<^sup>*)\<inverse>" by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI) lemma sym_rtrancl: "sym r \<Longrightarrow> sym (r\<^sup>*)"