doc-src/TutorialI/Inductive/AB.thy
changeset 16412 50eab0183aea
parent 12815 1f073030b97a
child 16585 02cf78f0afce
--- 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 \<Rightarrow> int"}, @{typ int} are the integers,
 @{text"\<bar>.\<bar>"} is the absolute value function\footnote{See
 Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii}