equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 % |
|
2 \begin{isabellebody}% |
2 \isanewline |
3 \isanewline |
3 \ \ \ \ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
4 \ \ \ \ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
4 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
5 \noindent\small |
6 \noindent\small |
6 where \isa{dvd} means ``divides''. |
7 where \isa{dvd} means ``divides''. |
7 Isabelle rejects this ``definition'' because of the extra \isa{m} on the |
8 Isabelle rejects this ``definition'' because of the extra \isa{m} on the |
8 right-hand side, which would introduce an inconsistency (why?). What you |
9 right-hand side, which would introduce an inconsistency (why?). What you |
9 should have written is% |
10 should have written is% |
10 \end{isamarkuptext}% |
11 \end{isamarkuptext}% |
11 \ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}\end{isabelle}% |
12 \ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}\end{isabellebody}% |
12 %%% Local Variables: |
13 %%% Local Variables: |
13 %%% mode: latex |
14 %%% mode: latex |
14 %%% TeX-master: "root" |
15 %%% TeX-master: "root" |
15 %%% End: |
16 %%% End: |