--- a/doc-src/TutorialI/Types/document/Numbers.tex Wed Jan 03 21:25:23 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Wed Jan 03 21:27:15 2001 +0100
@@ -2,7 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{Numbers}%
\isanewline
-\isacommand{theory}\ Numbers\ {\isacharequal}\ Main{\isacharcolon}\isanewline
+\isacommand{theory}\ Numbers\ {\isacharequal}\ Real{\isacharcolon}\isanewline
\isanewline
\isacommand{ML}\ {\isachardoublequote}Pretty{\isachardot}setmargin\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequote}%
\begin{isamarkuptext}%
@@ -231,6 +231,59 @@
\end{isabelle}
\rulename{abs_mult}%
\end{isamarkuptext}%
+%
+\begin{isamarkuptext}%
+REALS
+
+\begin{isabelle}%
+\ \ \ \ \ {\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n\ {\isacharequal}\ {\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}%
+\end{isabelle}
+\rulename{realpow_abs}
+
+\begin{isabelle}%
+\ \ \ \ \ x\ {\isacharless}\ y\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ x\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ y%
+\end{isabelle}
+\rulename{real_dense}
+
+\begin{isabelle}%
+\ \ \ \ \ {\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n\ {\isacharequal}\ {\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}%
+\end{isabelle}
+\rulename{realpow_abs}
+
+\begin{isabelle}%
+\ \ \ \ \ x\ {\isacharasterisk}\ {\isacharparenleft}y\ {\isacharslash}\ z{\isacharparenright}\ {\isacharequal}\ x\ {\isacharasterisk}\ y\ {\isacharslash}\ z%
+\end{isabelle}
+\rulename{real_times_divide1_eq}
+
+\begin{isabelle}%
+\ \ \ \ \ y\ {\isacharslash}\ z\ {\isacharasterisk}\ x\ {\isacharequal}\ y\ {\isacharasterisk}\ x\ {\isacharslash}\ z%
+\end{isabelle}
+\rulename{real_times_divide2_eq}
+
+\begin{isabelle}%
+\ \ \ \ \ x\ {\isacharslash}\ {\isacharparenleft}y\ {\isacharslash}\ z{\isacharparenright}\ {\isacharequal}\ x\ {\isacharasterisk}\ z\ {\isacharslash}\ y%
+\end{isabelle}
+\rulename{real_divide_divide1_eq}
+
+\begin{isabelle}%
+\ \ \ \ \ x\ {\isacharslash}\ y\ {\isacharslash}\ z\ {\isacharequal}\ x\ {\isacharslash}\ {\isacharparenleft}y\ {\isacharasterisk}\ z{\isacharparenright}%
+\end{isabelle}
+\rulename{real_divide_divide2_eq}
+
+\begin{isabelle}%
+\ \ \ \ \ {\isacharminus}\ x\ {\isacharslash}\ y\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}x\ {\isacharslash}\ y{\isacharparenright}%
+\end{isabelle}
+\rulename{real_minus_divide_eq}
+
+\begin{isabelle}%
+\ \ \ \ \ x\ {\isacharslash}\ {\isacharminus}\ y\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}x\ {\isacharslash}\ y{\isacharparenright}%
+\end{isabelle}
+\rulename{real_divide_minus_eq}
+
+This last NOT a simprule
+
+real_add_divide_distrib%
+\end{isamarkuptext}%
\isacommand{end}\isanewline
\end{isabellebody}%
%%% Local Variables: