| changeset 5278 | a903b66822e2 |
| parent 5183 | 89f162de39cf |
| child 5316 | 7a8975451a89 |
--- a/src/HOL/RelPow.ML Thu Aug 06 15:47:26 1998 +0200 +++ b/src/HOL/RelPow.ML Thu Aug 06 15:48:13 1998 +0200 @@ -57,8 +57,7 @@ qed_spec_mp "rel_pow_Suc_D2"; -Goal -"!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)"; +Goal "!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)"; by (nat_ind_tac "n" 1); by (fast_tac (claset() addss (simpset())) 1); by (fast_tac (claset() addss (simpset())) 1);