doc-src/TutorialI/Types/numerics.tex
changeset 33750 0a0d6d79d984
parent 31682 358cdcdf56d2
child 33760 15f9bd93a1dd
     1.1 --- a/doc-src/TutorialI/Types/numerics.tex	Wed Nov 18 14:00:08 2009 +0100
     1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Thu Nov 19 08:19:57 2009 +0100
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  \section{Numbers}
     1.6  \label{sec:numbers}
     1.7  
     1.8 @@ -192,7 +191,7 @@
     1.9  relation.  Here are some of the facts proved about it:
    1.10  \begin{isabelle}
    1.11  \isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%
    1.12 -\rulenamedx{dvd_anti_sym}\isanewline
    1.13 +\rulenamedx{dvd_antisym}\isanewline
    1.14  \isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)
    1.15  \rulenamedx{dvd_add}
    1.16  \end{isabelle}