diff -r 04cc6b4b3439 -r 50eab0183aea doc-src/TutorialI/Inductive/AB.thy --- a/doc-src/TutorialI/Inductive/AB.thy Thu Jun 16 11:38:52 2005 +0200 +++ b/doc-src/TutorialI/Inductive/AB.thy Thu Jun 16 18:25:54 2005 +0200 @@ -101,7 +101,7 @@ right increases or decreases the difference by 1, we must have passed through 1 on our way from 0 to 2. Formally, we appeal to the following discrete intermediate value theorem @{thm[source]nat0_intermed_int_val} -@{thm[display]nat0_intermed_int_val[no_vars]} +@{thm[display,margin=60]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\footnote{See Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii}