equal
deleted
inserted
replaced
55 by(induct_tac xs, auto); |
55 by(induct_tac xs, auto); |
56 (*>*) |
56 (*>*) |
57 |
57 |
58 text{*\noindent |
58 text{*\noindent |
59 This time, induction leaves us with the following base case |
59 This time, induction leaves us with the following base case |
|
60 %{goals[goals_limit=1,display]} |
60 \begin{isabelle} |
61 \begin{isabelle} |
61 \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ [] |
62 \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ [] |
62 \end{isabelle} |
63 \end{isabelle} |
63 which is trivial, and @{text"auto"} finishes the whole proof. |
64 which is trivial, and @{text"auto"} finishes the whole proof. |
64 |
65 |