equal
deleted
inserted
replaced
1 % |
1 \begin{isabelle}% |
2 \begin{isabellebody}% |
|
3 % |
2 % |
4 \begin{isamarkuptext}% |
3 \begin{isamarkuptext}% |
5 \noindent |
4 \noindent |
6 Now that we have learned about rules and logic, we take another look at the |
5 Now that we have learned about rules and logic, we take another look at the |
7 finer points of induction. The two questions we answer are: what to do if the |
6 finer points of induction. The two questions we answer are: what to do if the |
270 \end{quote} |
269 \end{quote} |
271 where \isa{wf\ \mbox{r}} means that the relation \isa{r} is wellfounded. |
270 where \isa{wf\ \mbox{r}} means that the relation \isa{r} is wellfounded. |
272 For example \isa{less\_induct} is the special case where \isa{r} is \isa{<} on \isa{nat}. |
271 For example \isa{less\_induct} is the special case where \isa{r} is \isa{<} on \isa{nat}. |
273 For details see the library.% |
272 For details see the library.% |
274 \end{isamarkuptext}% |
273 \end{isamarkuptext}% |
275 \end{isabellebody}% |
274 \end{isabelle}% |
276 %%% Local Variables: |
275 %%% Local Variables: |
277 %%% mode: latex |
276 %%% mode: latex |
278 %%% TeX-master: "root" |
277 %%% TeX-master: "root" |
279 %%% End: |
278 %%% End: |