equal
deleted
inserted
replaced
402 % |
402 % |
403 \begin{isamarkuptext}% |
403 \begin{isamarkuptext}% |
404 FIELDS |
404 FIELDS |
405 |
405 |
406 \begin{isabelle}% |
406 \begin{isabelle}% |
407 a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ a\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ b% |
407 a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachargreater}a{\isachardot}\ r\ {\isacharless}\ b% |
408 \end{isabelle} |
408 \end{isabelle} |
409 \rulename{dense} |
409 \rulename{dense} |
410 |
410 |
411 \begin{isabelle}% |
411 \begin{isabelle}% |
412 a\ {\isacharasterisk}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ b\ {\isacharslash}\ c% |
412 a\ {\isacharasterisk}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ b\ {\isacharslash}\ c% |