doc-src/TutorialI/Types/Numbers.thy

--- a/doc-src/TutorialI/Types/Numbers.thy	Mon Jan 12 16:45:35 2004 +0100
+++ b/doc-src/TutorialI/Types/Numbers.thy	Mon Jan 12 16:51:45 2004 +0100
@@ -197,14 +197,11 @@
 
 text {*REALS
 
-@{thm[display] realpow_abs[no_vars]}
-\rulename{realpow_abs}
-
 @{thm[display] dense[no_vars]}
 \rulename{dense}
 
-@{thm[display] realpow_abs[no_vars]}
-\rulename{realpow_abs}
+@{thm[display] power_abs[no_vars]}
+\rulename{power_abs}
 
 @{thm[display] times_divide_eq_right[no_vars]}
 \rulename{times_divide_eq_right}