doc-src/TutorialI/Types/numerics.tex
 changeset 14288 d149e3cbdb39 parent 13996 a994b92ab1ea child 14295 7f115e5c5de4
     1.1 --- a/doc-src/TutorialI/Types/numerics.tex	Wed Dec 10 14:29:44 2003 +0100
1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Wed Dec 10 15:59:34 2003 +0100
1.3 @@ -404,14 +404,14 @@
1.4  are installed as default simplification rules in order to express
1.5  combinations of products and quotients as rational expressions:
1.6  \begin{isabelle}
1.7 -x\ *\ (y\ /\ z)\ =\ x\ *\ y\ /\ z
1.8 -\rulename{real_times_divide1_eq}\isanewline
1.9 -y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z
1.10 -\rulename{real_times_divide2_eq}\isanewline
1.11 -x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y
1.12 -\rulename{real_divide_divide1_eq}\isanewline
1.13 -x\ /\ y\ /\ z\ =\ x\ /\ (y\ *\ z)
1.14 -\rulename{real_divide_divide2_eq}
1.15 +a\ *\ (b\ /\ c)\ =\ a\ *\ b\ /\ c
1.16 +\rulename{times_divide_eq_right}\isanewline
1.17 +b\ /\ c\ *\ a\ =\ b\ *\ a\ /\ c
1.18 +\rulename{times_divide_eq_left}\isanewline
1.19 +a\ /\ (b\ /\ c)\ =\ a\ *\ c\ /\ b
1.20 +\rulename{divide_divide_eq_right}\isanewline
1.21 +a\ /\ b\ /\ c\ =\ a\ /\ (b\ *\ c)
1.22 +\rulename{divide_divide_eq_left}
1.23  \end{isabelle}
1.24
1.25  Signs are extracted from quotients in the hope that complementary terms can