| changeset 5143 | b94cd208f073 |
| parent 5069 | 3ea049f7979d |
| child 5183 | 89f162de39cf |
--- a/src/HOL/RelPow.ML Tue Jul 14 13:33:12 1998 +0200 +++ b/src/HOL/RelPow.ML Wed Jul 15 10:15:13 1998 +0200 @@ -15,7 +15,7 @@ by (Simp_tac 1); qed "rel_pow_0_I"; -Goal "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)"; +Goal "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)"; by (Simp_tac 1); by (Blast_tac 1); qed "rel_pow_Suc_I";