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