src/HOL/RelPow.ML
changeset 3371 80f0d0b2f404
parent 3023 01364e2f30ad
child 4059 59c1422c9da5
--- a/src/HOL/RelPow.ML	Fri May 30 15:19:58 1997 +0200
+++ b/src/HOL/RelPow.ML	Fri May 30 15:20:41 1997 +0200
@@ -6,7 +6,7 @@
 
 open RelPow;
 
-goal RelPow.thy "R^1 = R";
+goal RelPow.thy "!!R:: ('a*'a)set. R^1 = R";
 by (Simp_tac 1);
 qed "rel_pow_1";
 Addsimps [rel_pow_1];