# HG changeset patch
# User wenzelm
# Date 1132786820 -3600
# Node ID 2215049cd29cfd6fc4774f48164e5f8b12bb3c3d
# Parent  afdba6b3e3833d9d6d7cee3034b86cf7edcfdb71
tuned induct proofs;

diff -r afdba6b3e383 -r 2215049cd29c src/HOL/Induct/Mutil.thy
--- a/src/HOL/Induct/Mutil.thy	Wed Nov 23 22:26:13 2005 +0100
+++ b/src/HOL/Induct/Mutil.thy	Thu Nov 24 00:00:20 2005 +0100
@@ -72,7 +72,7 @@
   done
 
 lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (2 * n) \<in> tiling domino"
-  by (induct m, auto)
+  by (induct m) auto
 
 
 text {* \medskip @{term coloured} and Dominoes *}
@@ -98,7 +98,7 @@
 text {* \medskip Tilings of dominoes *}
 
 lemma tiling_domino_finite [simp]: "t \<in> tiling domino ==> finite t"
-  by (induct set: tiling, auto)
+  by (induct set: tiling) auto
 
 declare
   Int_Un_distrib [simp]
diff -r afdba6b3e383 -r 2215049cd29c src/HOL/Induct/QuoNestedDataType.thy
--- a/src/HOL/Induct/QuoNestedDataType.thy	Wed Nov 23 22:26:13 2005 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy	Thu Nov 24 00:00:20 2005 +0100
@@ -265,7 +265,7 @@
 
 lemma listset_Rep_Exp_Abs_Exp:
      "listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel `` {Us}";
-by (induct_tac Us, simp_all add: listrel_Cons Abs_ExpList_def)
+by (induct Us, simp_all add: listrel_Cons Abs_ExpList_def)
 
 lemma FnCall:
      "FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})"
@@ -459,4 +459,3 @@
 qed
 
 end
-
diff -r afdba6b3e383 -r 2215049cd29c src/HOL/Induct/Tree.thy
--- a/src/HOL/Induct/Tree.thy	Wed Nov 23 22:26:13 2005 +0100
+++ b/src/HOL/Induct/Tree.thy	Thu Nov 24 00:00:20 2005 +0100
@@ -46,7 +46,7 @@
   "add i (Lim f) = Lim (%n. add i (f n))"
 
 lemma add_assoc: "add (add i j) k = add i (add j k)"
-by (induct k, auto)
+  by (induct k) auto
 
 text{*Multiplication of ordinals*}
 consts
@@ -57,14 +57,10 @@
   "mult i (Lim f) = Lim (%n. mult i (f n))"
 
 lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
-apply (induct k) 
-apply (auto simp add: add_assoc) 
-done
+  by (induct k) (auto simp add: add_assoc)
 
 lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
-apply (induct k) 
-apply (auto simp add: add_mult_distrib) 
-done
+  by (induct k) (auto simp add: add_mult_distrib)
 
 text{*We could probably instantiate some axiomatic type classes and use
 the standard infix operators.*}
@@ -104,7 +100,6 @@
   (hints recdef_wf: wf_brouwer_order)
 
 lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))"
-by (induct k, auto)
-
+  by (induct k) auto
 
 end