equal
deleted
inserted
replaced
74 empty list, the singleton list, and the list with at least two elements. |
74 empty list, the singleton list, and the list with at least two elements. |
75 The final case has an induction hypothesis: you may assume that \isa{P} |
75 The final case has an induction hypothesis: you may assume that \isa{P} |
76 holds for the tail of that list.% |
76 holds for the tail of that list.% |
77 \end{isamarkuptext}% |
77 \end{isamarkuptext}% |
78 \isamarkuptrue% |
78 \isamarkuptrue% |
|
79 \isanewline |
79 \isamarkupfalse% |
80 \isamarkupfalse% |
80 \end{isabellebody}% |
81 \end{isabellebody}% |
81 %%% Local Variables: |
82 %%% Local Variables: |
82 %%% mode: latex |
83 %%% mode: latex |
83 %%% TeX-master: "root" |
84 %%% TeX-master: "root" |