equal
deleted
inserted
replaced
83 \begin{isamarkuptxt}% |
83 \begin{isamarkuptxt}% |
84 \noindent |
84 \noindent |
85 The proof is canonical:% |
85 The proof is canonical:% |
86 \end{isamarkuptxt}% |
86 \end{isamarkuptxt}% |
87 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ b{\isacharparenright}\isanewline |
87 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ b{\isacharparenright}\isanewline |
88 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}% |
88 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline |
|
89 \isacommand{done}% |
89 \begin{isamarkuptext}% |
90 \begin{isamarkuptext}% |
90 \noindent |
91 \noindent |
91 In fact, all proofs in this case study look exactly like this. Hence we do |
92 In fact, all proofs in this case study look exactly like this. Hence we do |
92 not show them below. |
93 not show them below. |
93 |
94 |