doc-src/TutorialI/Types/document/Numbers.tex
changeset 25056 743f3603ba8b
parent 23504 2b2323124e8e
child 27376 ffe9b958bada
     1.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex	Tue Oct 16 17:06:21 2007 +0200
     1.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex	Tue Oct 16 17:07:40 2007 +0200
     1.3 @@ -404,7 +404,7 @@
     1.4  FIELDS
     1.5  
     1.6  \begin{isabelle}%
     1.7 -a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachargreater}a{\isachardot}\ r\ {\isacharless}\ b%
     1.8 +x\ {\isacharless}\ y\ {\isasymLongrightarrow}\ {\isasymexists}z{\isachargreater}x{\isachardot}\ z\ {\isacharless}\ y%
     1.9  \end{isabelle}
    1.10  \rulename{dense}
    1.11