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