# HG changeset patch
# User wenzelm
# Date 978553635 -3600
# Node ID 985066e9495d261a0bd3956aa8963e01188358d0
# Parent  3a5e5657e41c5a7f0181c108ce13ef0ad32649d4
updated;

diff -r 3a5e5657e41c -r 985066e9495d doc-src/TutorialI/Types/document/Numbers.tex
--- 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: