diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/fp.tex	Thu Jan 25 15:31:31 2001 +0100
@@ -129,10 +129,10 @@
   \isa{\isacommand{theory}~T~=~\dots~:} is processed, the
   modified parent is reloaded automatically.
   
-  The only time when you need to load a theory by hand is when you simply
-  want to check if it loads successfully without wanting to make use of the
-  theory itself. This you can do by typing
-  \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
+%  The only time when you need to load a theory by hand is when you simply
+%  want to check if it loads successfully without wanting to make use of the
+%  theory itself. This you can do by typing
+%  \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
 \end{description}
 Further commands are found in the Isabelle/Isar Reference Manual.
 
@@ -302,7 +302,7 @@
 section as well, in particular in order to understand what happened if things
 do not simplify as expected.
 
-\subsubsection{What is Simplification?}
+\subsubsection{What is Simplification}
 
 In its most basic form, simplification means repeated application of
 equations from left to right. For example, taking the rules for \isa{\at}