src/HOL/Transitive_Closure.thy
changeset 20716 a6686a8e1b68
parent 19656 09be06943252
child 21210 c17fd2df4e9e
--- a/src/HOL/Transitive_Closure.thy	Tue Sep 26 13:34:35 2006 +0200
+++ b/src/HOL/Transitive_Closure.thy	Tue Sep 26 17:33:04 2006 +0200
@@ -208,7 +208,7 @@
   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)
 
 
@@ -263,7 +263,7 @@
 
 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^+)"