author | haftmann |
Sat, 24 Dec 2011 15:53:12 +0100 | |
changeset 45976 | 9dc0d950baa9 |
parent 45975 | 5e78c499a7ff |
child 45977 | e3accf78bb07 |
--- 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 = {}"