1.1 --- a/src/HOL/Transitive_Closure.thy	Sat Dec 24 15:53:12 2011 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Sat Dec 24 15:53:12 2011 +0100
     1.3 @@ -773,10 +773,10 @@
     1.4    done
     1.5  
     1.6  lemma rel_pow_add: "R ^^ (m+n) = R^^m O R^^n"
     1.7 -by(induct n) auto
     1.8 +  by (induct n) auto
     1.9  
    1.10  lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R"
    1.11 -by (induct n) (simp, simp add: O_assoc [symmetric])
    1.12 +  by (induct n) (simp, simp add: O_assoc [symmetric])
    1.13  
    1.14  lemma rel_pow_empty:
    1.15    "0 < n \<Longrightarrow> ({} :: ('a \<times> 'a) set) ^^ n = {}"