| changeset 4477 | b3e5857d8d99 |
| parent 4387 | 31d5a5a191e8 |
| child 4686 | 74a12e86b20b |
--- a/src/HOL/Induct/Mutil.ML Tue Dec 23 11:56:09 1997 +0100 +++ b/src/HOL/Induct/Mutil.ML Wed Dec 24 10:02:30 1997 +0100 @@ -53,7 +53,7 @@ \ {(i, n+n), (i, Suc(n+n))}" 1); by (Blast_tac 2); by (asm_simp_tac (simpset() addsimps [domino.horiz]) 1); -by (Auto_tac()); +by Auto_tac; qed "dominoes_tile_row"; goal thy "(below m) Times below(n+n) : tiling domino";