| changeset 2056 | 93c093620c28 |
| parent 2031 | 03a843f0f447 |
| child 2741 | 2b7f72cbe51f |
--- a/src/HOL/RelPow.ML Mon Oct 07 10:26:00 1996 +0200 +++ b/src/HOL/RelPow.ML Mon Oct 07 10:28:44 1996 +0200 @@ -26,7 +26,6 @@ goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n --> (x,z):R^(Suc n)"; by (nat_ind_tac "n" 1); by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1); -by (Fast_tac 1); by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1); by (Fast_tac 1); qed_spec_mp "rel_pow_Suc_I2";