--- 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}