# HG changeset patch # User paulson # Date 864998441 -7200 # Node ID 80f0d0b2f4044c499a6ef81886cc4a37f00770ef # Parent 5c5fdce3a4e4fd5001cd04631ca74e15672bd55b Overloading of "^" requires a type constraint diff -r 5c5fdce3a4e4 -r 80f0d0b2f404 src/HOL/RelPow.ML --- 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];