| changeset 29927 | ae8f42c245b2 |
| parent 29856 | 984191be0357 |
| child 30008 | 20c194b71bb7 |
| child 30240 | 5b25fee0362c |
--- a/src/HOL/List.thy Mon Feb 16 10:11:20 2009 +0100 +++ b/src/HOL/List.thy Mon Feb 16 10:13:30 2009 +0100 @@ -257,7 +257,7 @@ \caption{Characteristic examples} \label{fig:Characteristic} \end{figure} -Figure~\ref{fig:Characteristic} shows charachteristic examples +Figure~\ref{fig:Characteristic} shows characteristic examples that should give an intuitive understanding of the above functions. *}