--- 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]
--- 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
-
--- 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