equal
deleted
inserted
replaced
17 \noindent |
17 \noindent |
18 and induction, for example% |
18 and induction, for example% |
19 \end{isamarkuptext}% |
19 \end{isamarkuptext}% |
20 \isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline |
20 \isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline |
21 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline |
21 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline |
22 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline |
22 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline |
|
23 \isacommand{done}\isanewline |
23 \end{isabellebody}% |
24 \end{isabellebody}% |
24 %%% Local Variables: |
25 %%% Local Variables: |
25 %%% mode: latex |
26 %%% mode: latex |
26 %%% TeX-master: "root" |
27 %%% TeX-master: "root" |
27 %%% End: |
28 %%% End: |