# HG changeset patch
# User haftmann
# Date 1324738392 -3600
# Node ID 9dc0d950baa9fd1464cd5c1147dc687813f0c36a
# Parent  5e78c499a7ffa373e22e7147293fec72110086f9
tuned layout

diff -r 5e78c499a7ff -r 9dc0d950baa9 src/HOL/Transitive_Closure.thy
--- 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 = {}"