src/HOL/Hyperreal/NatStar.thy
changeset 15085 5693a977a767
parent 14641 79b7bd936264
child 15131 c69542757a4d
--- a/src/HOL/Hyperreal/NatStar.thy	Thu Jul 29 16:14:06 2004 +0200
+++ b/src/HOL/Hyperreal/NatStar.thy	Thu Jul 29 16:14:42 2004 +0200
@@ -7,7 +7,7 @@
 
 header{*Star-transforms for the Hypernaturals*}
 
-theory NatStar = RealPow + HyperPow:
+theory NatStar = "../Real/RealPow" + HyperPow:
 
 
 text{*Extends sets of nats, and functions from the nats to nats or reals*}