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