1.1 --- a/src/HOL/Induct/Tree.thy	Wed Nov 23 22:26:13 2005 +0100
     1.2 +++ b/src/HOL/Induct/Tree.thy	Thu Nov 24 00:00:20 2005 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4    "add i (Lim f) = Lim (%n. add i (f n))"
     1.5  
     1.6  lemma add_assoc: "add (add i j) k = add i (add j k)"
     1.7 -by (induct k, auto)
     1.8 +  by (induct k) auto
     1.9  
    1.10  text{*Multiplication of ordinals*}
    1.11  consts
    1.12 @@ -57,14 +57,10 @@
    1.13    "mult i (Lim f) = Lim (%n. mult i (f n))"
    1.14  
    1.15  lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
    1.16 -apply (induct k) 
    1.17 -apply (auto simp add: add_assoc) 
    1.18 -done
    1.19 +  by (induct k) (auto simp add: add_assoc)
    1.20  
    1.21  lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
    1.22 -apply (induct k) 
    1.23 -apply (auto simp add: add_mult_distrib) 
    1.24 -done
    1.25 +  by (induct k) (auto simp add: add_mult_distrib)
    1.26  
    1.27  text{*We could probably instantiate some axiomatic type classes and use
    1.28  the standard infix operators.*}
    1.29 @@ -104,7 +100,6 @@
    1.30    (hints recdef_wf: wf_brouwer_order)
    1.31  
    1.32  lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))"
    1.33 -by (induct k, auto)
    1.34 -
    1.35 +  by (induct k) auto
    1.36  
    1.37  end