src/HOL/Hyperreal/HyperPow.thy

--- a/src/HOL/Hyperreal/HyperPow.thy	Fri Jan 05 18:33:47 2001 +0100
+++ b/src/HOL/Hyperreal/HyperPow.thy	Fri Jan 05 18:48:18 2001 +0100
@@ -32,5 +32,5 @@
   hyperpow_def
   "(R::hypreal) pow (N::hypnat) 
       == Abs_hypreal(UN X:Rep_hypreal(R). UN Y: Rep_hypnat(N).
-             hyprel^^{%n::nat. (X n) ^ (Y n)})"
+             hyprel```{%n::nat. (X n) ^ (Y n)})"
 end