# HG changeset patch
# User paulson
# Date 958478669 -7200
# Node ID f797816932d7269788b6963e1db473c6de16f8d3
# Parent  ac86b3d4473016fe9a334ee28c1d23a4f6e53701
reverted to old proof of dominoes_tile_row, given new treatment of #2+...

diff -r ac86b3d44730 -r f797816932d7 src/HOL/Induct/Mutil.ML
--- a/src/HOL/Induct/Mutil.ML	Mon May 15 17:34:05 2000 +0200
+++ b/src/HOL/Induct/Mutil.ML	Tue May 16 14:04:29 2000 +0200
@@ -37,20 +37,19 @@
 qed "Sigma_Suc1";
 
 Goalw [below_def]
-    "A <*> below(#2+n) = (A <*> {n}) Un (A <*> {Suc n}) Un (A <*> (below n))";
+    "A <*> below(Suc n) = (A <*> {n}) Un (A <*> (below n))";
 by Auto_tac;
-by (arith_tac 1);
 qed "Sigma_Suc2";
 
 Addsimps [Sigma_Suc1, Sigma_Suc2];
 
-Goal "({i} <*> {m}) Un ({i} <*> {n}) = {(i,m), (i,n)}";
+Goal "({i} <*> {n}) Un ({i} <*> {m}) = {(i,m), (i,n)}";
 by Auto_tac;
 qed "sing_Times_lemma";
 
 Goal "{i} <*> below(#2*n) : tiling domino";
 by (induct_tac "n" 1);
-by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_assoc RS sym])));
 by (rtac tiling.Un 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [sing_Times_lemma])));
 qed "dominoes_tile_row";