1.1 --- a/src/HOL/Transitive_Closure.thy	Tue Sep 26 13:34:35 2006 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Tue Sep 26 17:33:04 2006 +0200
     1.3 @@ -208,7 +208,7 @@
     1.4    by (blast elim: rtranclE converse_rtranclE
     1.5      intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)
     1.6  
     1.7 -lemma rtrancl_unfold: "r^* = Id Un (r O r^*)"
     1.8 +lemma rtrancl_unfold: "r^* = Id Un r O r^*"
     1.9    by (auto intro: rtrancl_into_rtrancl elim: rtranclE)
    1.10  
    1.11  
    1.12 @@ -263,7 +263,7 @@
    1.13  
    1.14  inductive_cases tranclE: "(a, b) : r^+"
    1.15  
    1.16 -lemma trancl_unfold: "r^+ = r Un (r O r^+)"
    1.17 +lemma trancl_unfold: "r^+ = r Un r O r^+"
    1.18    by (auto intro: trancl_into_trancl elim: tranclE)
    1.19  
    1.20  lemma trans_trancl[simp]: "trans(r^+)"