doc-src/Locales/Locales/document/Examples3.tex
changeset 35423 6ef9525a5727
parent 33868 62251d6b0038
child 37206 7f2a6f3143ad
equal deleted inserted replaced
35422:e74b6f3b950c 35423:6ef9525a5727
   139 	\begin{isabelle}%
   139 	\begin{isabelle}%
   140 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}inf{\isasymle}x{\isachardot}\ inf\ {\isasymle}\ y\ {\isasymand}\ {\isacharparenleft}{\isasymforall}z{\isachardot}\ z\ {\isasymle}\ x\ {\isasymand}\ z\ {\isasymle}\ y\ {\isasymlongrightarrow}\ z\ {\isasymle}\ inf{\isacharparenright}\isanewline
   140 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}inf{\isasymle}x{\isachardot}\ inf\ {\isasymle}\ y\ {\isasymand}\ {\isacharparenleft}{\isasymforall}z{\isachardot}\ z\ {\isasymle}\ x\ {\isasymand}\ z\ {\isasymle}\ y\ {\isasymlongrightarrow}\ z\ {\isasymle}\ inf{\isacharparenright}\isanewline
   141 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}sup{\isasymge}x{\isachardot}\ y\ {\isasymle}\ sup\ {\isasymand}\ {\isacharparenleft}{\isasymforall}z{\isachardot}\ x\ {\isasymle}\ z\ {\isasymand}\ y\ {\isasymle}\ z\ {\isasymlongrightarrow}\ sup\ {\isasymle}\ z{\isacharparenright}%
   141 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}sup{\isasymge}x{\isachardot}\ y\ {\isasymle}\ sup\ {\isasymand}\ {\isacharparenleft}{\isasymforall}z{\isachardot}\ x\ {\isasymle}\ z\ {\isasymand}\ y\ {\isasymle}\ z\ {\isasymlongrightarrow}\ sup\ {\isasymle}\ z{\isacharparenright}%
   142 \end{isabelle}
   142 \end{isabelle}
   143 	This is Presburger arithmetic, which can be solved by the
   143 	This is Presburger arithmetic, which can be solved by the
   144 	method \isa{arith}.%
   144         method \isa{arith}.%
   145 \end{isamarkuptxt}%
   145 \end{isamarkuptxt}%
   146 \isamarkuptrue%
   146 \isamarkuptrue%
   147 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
   147 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
   148 \ arith{\isacharplus}%
   148 \ arith{\isacharplus}%
   149 \begin{isamarkuptxt}%
   149 \begin{isamarkuptxt}%