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