src/HOL/Transitive_Closure.thy

 
 lemma r_comp_rtrancl_eq: "r O r^* = r^* O r"
   by (blast elim: rtranclE converse_rtranclE
     intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)
 
-lemma rtrancl_unfold: "r^* = Id Un (r O r^*)"
+lemma rtrancl_unfold: "r^* = Id Un r O r^*"
   by (auto intro: rtrancl_into_rtrancl elim: rtranclE)
 
 
 subsection {* Transitive closure *}
 

   -- {* Another induction rule for trancl, incorporating transitivity *}
   by (iprover intro: r_into_trancl major [THEN trancl_induct] cases)
 
 inductive_cases tranclE: "(a, b) : r^+"
 
-lemma trancl_unfold: "r^+ = r Un (r O r^+)"
+lemma trancl_unfold: "r^+ = r Un r O r^+"
   by (auto intro: trancl_into_trancl elim: tranclE)
 
 lemma trans_trancl[simp]: "trans(r^+)"
   -- {* Transitivity of @{term "r^+"} *}
 proof (rule transI)