1.1 --- a/doc-src/TutorialI/basics.tex	Thu Dec 02 00:44:54 2004 +0100
     1.2 +++ b/doc-src/TutorialI/basics.tex	Thu Dec 02 10:36:20 2004 +0100
     1.3 @@ -57,7 +57,7 @@
     1.4  begin
     1.5  {\rmfamily\textit{declarations, definitions, and proofs}}
     1.6  end
     1.7 -\end{ttbox}
     1.8 +\end{ttbox}\cmmdx{theory}\cmmdx{imports}
     1.9  where \texttt{B}$@1$ \dots\ \texttt{B}$@n$ are the names of existing
    1.10  theories that \texttt{T} is based on and \textit{declarations,
    1.11      definitions, and proofs} represents the newly introduced concepts

     2.1 --- a/doc-src/TutorialI/fp.tex	Thu Dec 02 00:44:54 2004 +0100
     2.2 +++ b/doc-src/TutorialI/fp.tex	Thu Dec 02 10:36:20 2004 +0100
     2.3 @@ -136,18 +136,17 @@
     2.4    \commdx{typ} \textit{string} reads and prints the given
     2.5    string as a type in the current context.
     2.6  \item[(Re)loading theories:] When you start your interaction you must open a
     2.7 -  named theory with the line \commdx{theory}~\isa{T~=~\dots~:}. Isabelle
     2.8 -  automatically loads all the required parent theories from their respective
     2.9 -  files (which may take a moment, unless the theories are already loaded and
    2.10 -  the files have not been modified).
    2.11 +  named theory with \commdx{theory}~\isa{T} \isacommand{imports} \dots
    2.12 +  \isacommand{begin}. Isabelle automatically loads all the required parent
    2.13 +  theories from their respective files (which may take a moment, unless the
    2.14 +  theories are already loaded and the files have not been modified).
    2.15    
    2.16    If you suddenly discover that you need to modify a parent theory of your
    2.17    current theory, you must first abandon your current theory%
    2.18 -  \indexbold{abandoning a theory}\indexbold{theories!abandoning} 
    2.19 -  (at the shell
    2.20 -  level type \commdx{kill}). After the parent theory has
    2.21 -  been modified, you go back to your original theory. When its first line
    2.22 -  \isa{\isacommand{theory}~T~=~\dots~:} is processed, the
    2.23 +  \indexbold{abandoning a theory}\indexbold{theories!abandoning} (at the
    2.24 +  shell level type \commdx{kill}). After the parent theory has been modified,
    2.25 +  you go back to your original theory. When its opening
    2.26 +  \isacommand{theory}~\isa{T} \dots \isacommand{begin} is processed, the
    2.27    modified parent is reloaded automatically.
    2.28    
    2.29  %  The only time when you need to load a theory by hand is when you simply