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