equal
deleted
inserted
replaced
24 qed "rel_pow_Suc_I"; |
24 qed "rel_pow_Suc_I"; |
25 |
25 |
26 goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n --> (x,z):R^(Suc n)"; |
26 goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n --> (x,z):R^(Suc n)"; |
27 by (nat_ind_tac "n" 1); |
27 by (nat_ind_tac "n" 1); |
28 by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1); |
28 by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1); |
29 by (Fast_tac 1); |
|
30 by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1); |
29 by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1); |
31 by (Fast_tac 1); |
30 by (Fast_tac 1); |
32 qed_spec_mp "rel_pow_Suc_I2"; |
31 qed_spec_mp "rel_pow_Suc_I2"; |
33 |
32 |
34 goal RelPow.thy "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P"; |
33 goal RelPow.thy "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P"; |