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