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