diff -r 891fbd3f4881 -r b28bbb153603 doc-src/TutorialI/Inductive/AB.thy --- a/doc-src/TutorialI/Inductive/AB.thy Fri May 18 12:13:53 2001 +0200 +++ b/doc-src/TutorialI/Inductive/AB.thy Fri May 18 16:45:55 2001 +0200 @@ -102,8 +102,9 @@ intermediate value theorem @{thm[source]nat0_intermed_int_val} @{thm[display]nat0_intermed_int_val[no_vars]} where @{term f} is of type @{typ"nat \ int"}, @{typ int} are the integers, -@{text"\.\"} is the absolute value function, and @{term"#1::int"} is the -integer 1 (see \S\ref{sec:numbers}). +@{text"\.\"} is the absolute value function\footnote{See +Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii} +syntax.}, and @{term"#1::int"} is the integer 1 (see \S\ref{sec:numbers}). First we show that our specific function, the difference between the numbers of @{term a}'s and @{term b}'s, does indeed only change by 1 in every