equal
deleted
inserted
replaced
318 % |
318 % |
319 \begin{isamarkuptext}% |
319 \begin{isamarkuptext}% |
320 REALS |
320 REALS |
321 |
321 |
322 \begin{isabelle}% |
322 \begin{isabelle}% |
323 {\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n% |
|
324 \end{isabelle} |
|
325 \rulename{realpow_abs} |
|
326 |
|
327 \begin{isabelle}% |
|
328 a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ a\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ b% |
323 a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ a\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ b% |
329 \end{isabelle} |
324 \end{isabelle} |
330 \rulename{dense} |
325 \rulename{dense} |
331 |
326 |
332 \begin{isabelle}% |
327 \begin{isabelle}% |
333 {\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n% |
328 {\isasymbar}a\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharcircum}\ n% |
334 \end{isabelle} |
329 \end{isabelle} |
335 \rulename{realpow_abs} |
330 \rulename{power_abs} |
336 |
331 |
337 \begin{isabelle}% |
332 \begin{isabelle}% |
338 a\ {\isacharasterisk}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ b\ {\isacharslash}\ c% |
333 a\ {\isacharasterisk}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ b\ {\isacharslash}\ c% |
339 \end{isabelle} |
334 \end{isabelle} |
340 \rulename{times_divide_eq_right} |
335 \rulename{times_divide_eq_right} |