changeset 45976 | 9dc0d950baa9 |
parent 45607 | 16b4f5774621 |
child 46127 | af3b95160b59 |
--- a/src/HOL/Transitive_Closure.thy Sat Dec 24 15:53:12 2011 +0100 +++ b/src/HOL/Transitive_Closure.thy Sat Dec 24 15:53:12 2011 +0100 @@ -773,10 +773,10 @@ done lemma rel_pow_add: "R ^^ (m+n) = R^^m O R^^n" -by(induct n) auto + by (induct n) auto lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R" -by (induct n) (simp, simp add: O_assoc [symmetric]) + by (induct n) (simp, simp add: O_assoc [symmetric]) lemma rel_pow_empty: "0 < n \<Longrightarrow> ({} :: ('a \<times> 'a) set) ^^ n = {}"