src/HOL/RelPow.ML
changeset 2031 03a843f0f447
parent 1760 6f41a494f3b1
child 2056 93c093620c28
     1.1 --- a/src/HOL/RelPow.ML	Thu Sep 26 11:11:22 1996 +0200
     1.2 +++ b/src/HOL/RelPow.ML	Thu Sep 26 12:47:47 1996 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  Addsimps [rel_pow_0];
     1.5  
     1.6  goal RelPow.thy "R^1 = R";
     1.7 -by(simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
     1.8 +by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
     1.9  qed "rel_pow_1";
    1.10  Addsimps [rel_pow_1];
    1.11