# HG changeset patch
# User nipkow
# Date 1225968770 -3600
# Node ID a08c37b478b2d17fab15cbce8a50bc7049b6ac53
# Parent  01e04e41cc7b0fa6136cb4f4f43e464a9ccb14ed
tuned

diff -r 01e04e41cc7b -r a08c37b478b2 src/HOL/Induct/Mutil.thy
--- a/src/HOL/Induct/Mutil.thy	Thu Nov 06 11:52:42 2008 +0100
+++ b/src/HOL/Induct/Mutil.thy	Thu Nov 06 11:52:50 2008 +0100
@@ -222,6 +222,8 @@
 
 text{* The main theorem: *}
 
+declare [[max_clauses = 200]]
+
 theorem Ls_can_tile: "i \<le> a \<Longrightarrow> a < 2^n + i \<Longrightarrow> j \<le> b \<Longrightarrow> b < 2^n + j
   \<Longrightarrow> square2 n i j - {(a,b)} : tiling Ls"
 proof(induct n arbitrary: a b i j)
@@ -302,12 +304,7 @@
     using a b by(simp add:L3_def) arith moreover
   have "?D \<Longrightarrow> L2 (2^n + i - 1) (2^n + j - 1) \<subseteq> square2 (n+1) i j - {(a, b)}"
     using a b by(simp add:L2_def) arith
-  ultimately show ?case
-    apply simp
-    apply(erule disjE)
-    apply (metis LinLs tiling_Diff1E)
-    apply (metis LinLs tiling_Diff1E)
-    done
+  ultimately show ?case by simp (metis LinLs tiling_Diff1E)
 qed
 
 corollary Ls_can_tile00: