src/HOL/Divides.ML
changeset 9637 47d39a31eb2f
parent 9108 9fff97d29837
child 9870 2374ba026fc6
     1.1 --- a/src/HOL/Divides.ML	Thu Aug 17 12:01:09 2000 +0200
     1.2 +++ b/src/HOL/Divides.ML	Thu Aug 17 12:02:01 2000 +0200
     1.3 @@ -424,7 +424,6 @@
     1.4  Goalw [dvd_def]  "!!k::nat. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
     1.5  by (etac exE 1);
     1.6  by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
     1.7 -by (Blast_tac 1);
     1.8  qed "dvd_mult_cancel";
     1.9  
    1.10  Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> (i*j) dvd (m*n :: nat)";