changeset 12304 | 8df202daf55d |
parent 11701 | 3d51fbf81c17 |
--- a/src/HOL/Divides.ML Wed Nov 28 00:37:08 2001 +0100 +++ b/src/HOL/Divides.ML Wed Nov 28 00:37:40 2001 +0100 @@ -508,12 +508,10 @@ Goalw [dvd_def] "n = m * k ==> m dvd n"; by (Blast_tac 1); qed "dvdI"; -AddXIs [dvdI]; Goalw [dvd_def] "!!P. [|m dvd n; !!k. n = m*k ==> P|] ==> P"; by (Blast_tac 1); qed "dvdE"; -AddXEs [dvdE]; Goalw [dvd_def] "m dvd (0::nat)"; by (blast_tac (claset() addIs [mult_0_right RS sym]) 1);