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

 {\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n%
 \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}
+a\ {\isacharasterisk}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ b\ {\isacharslash}\ c%
+\end{isabelle}
+\rulename{times_divide_eq_right}
+
+\begin{isabelle}%
+b\ {\isacharslash}\ c\ {\isacharasterisk}\ a\ {\isacharequal}\ b\ {\isacharasterisk}\ a\ {\isacharslash}\ c%
+\end{isabelle}
+\rulename{times_divide_eq_left}
+
+\begin{isabelle}%
+a\ {\isacharslash}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ c\ {\isacharslash}\ b%
+\end{isabelle}
+\rulename{divide_divide_eq_right}
+
+\begin{isabelle}%
+a\ {\isacharslash}\ b\ {\isacharslash}\ c\ {\isacharequal}\ a\ {\isacharslash}\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}%
+\end{isabelle}
+\rulename{divide_divide_eq_left}
 
 \begin{isabelle}%
 {\isacharminus}\ x\ {\isacharslash}\ y\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}x\ {\isacharslash}\ y{\isacharparenright}%
 \end{isabelle}
 \rulename{real_minus_divide_eq}