author nipkow Thu, 06 Nov 2008 11:52:50 +0100 changeset 28720 a08c37b478b2 parent 28719 01e04e41cc7b child 28721 21170e10c745
tuned
 src/HOL/Induct/Mutil.thy file | annotate | diff | comparison | revisions
```--- 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:```