doc-src/TutorialI/Types/document/Numbers.tex

 %
 \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}%
 numeric literals; default simprules; can re-orient%
 \end{isamarkuptext}%

 
 \begin{isabelle}%
 \ \ \ \ \ {\isasymbar}x\ {\isacharasterisk}\ y{\isasymbar}\ {\isacharequal}\ {\isasymbar}x{\isasymbar}\ {\isacharasterisk}\ {\isasymbar}y{\isasymbar}%
 \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:
 %%% mode: latex