# HG changeset patch
# User wenzelm
# Date 1125325082 -7200
# Node ID ae84287f44e3ccdc5c1f91aa6bdf6eea6661388b
# Parent  5f42dd5e657076c25dbe8772835f32760ba4d4b7
tune spacing where a generated theory text is included directly;

diff -r 5f42dd5e6570 -r ae84287f44e3 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Mon Aug 29 11:44:23 2005 +0200
+++ b/doc-src/TutorialI/fp.tex	Mon Aug 29 16:18:02 2005 +0200
@@ -32,7 +32,7 @@
 \end{figure}
 
 \index{*ToyList example|(}
-{\makeatother\input{ToyList/document/ToyList.tex}}
+{\makeatother\medskip\input{ToyList/document/ToyList.tex}}
 
 The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The
 concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs}
@@ -216,7 +216,7 @@
 \label{sec:nat}\index{natural numbers}%
 \index{linear arithmetic|(}
 
-\input{Misc/document/fakenat.tex}
+\input{Misc/document/fakenat.tex}\medskip
 \input{Misc/document/natsum.tex}
 
 \index{linear arithmetic|)}
@@ -245,6 +245,7 @@
 Type synonyms are similar to those found in ML\@. They are created by a 
 \commdx{types} command:
 
+\medskip
 \input{Misc/document/types.tex}
 
 \input{Misc/document/prime_def.tex}