1.1 --- a/doc-src/TutorialI/fp.tex	Thu Jan 25 11:59:52 2001 +0100
     1.2 +++ b/doc-src/TutorialI/fp.tex	Thu Jan 25 15:31:31 2001 +0100
     1.3 @@ -129,10 +129,10 @@
     1.4    \isa{\isacommand{theory}~T~=~\dots~:} is processed, the
     1.5    modified parent is reloaded automatically.
     1.6    
     1.7 -  The only time when you need to load a theory by hand is when you simply
     1.8 -  want to check if it loads successfully without wanting to make use of the
     1.9 -  theory itself. This you can do by typing
    1.10 -  \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
    1.11 +%  The only time when you need to load a theory by hand is when you simply
    1.12 +%  want to check if it loads successfully without wanting to make use of the
    1.13 +%  theory itself. This you can do by typing
    1.14 +%  \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
    1.15  \end{description}
    1.16  Further commands are found in the Isabelle/Isar Reference Manual.
    1.17  
    1.18 @@ -302,7 +302,7 @@
    1.19  section as well, in particular in order to understand what happened if things
    1.20  do not simplify as expected.
    1.21  
    1.22 -\subsubsection{What is Simplification?}
    1.23 +\subsubsection{What is Simplification}
    1.24  
    1.25  In its most basic form, simplification means repeated application of
    1.26  equations from left to right. For example, taking the rules for \isa{\at}