1.1 --- a/doc-src/TutorialI/fp.tex	Thu Dec 02 00:44:54 2004 +0100
     1.2 +++ b/doc-src/TutorialI/fp.tex	Thu Dec 02 10:36:20 2004 +0100
     1.3 @@ -136,18 +136,17 @@
     1.4    \commdx{typ} \textit{string} reads and prints the given
     1.5    string as a type in the current context.
     1.6  \item[(Re)loading theories:] When you start your interaction you must open a
     1.7 -  named theory with the line \commdx{theory}~\isa{T~=~\dots~:}. Isabelle
     1.8 -  automatically loads all the required parent theories from their respective
     1.9 -  files (which may take a moment, unless the theories are already loaded and
    1.10 -  the files have not been modified).
    1.11 +  named theory with \commdx{theory}~\isa{T} \isacommand{imports} \dots
    1.12 +  \isacommand{begin}. Isabelle automatically loads all the required parent
    1.13 +  theories from their respective files (which may take a moment, unless the
    1.14 +  theories are already loaded and the files have not been modified).
    1.15    
    1.16    If you suddenly discover that you need to modify a parent theory of your
    1.17    current theory, you must first abandon your current theory%
    1.18 -  \indexbold{abandoning a theory}\indexbold{theories!abandoning} 
    1.19 -  (at the shell
    1.20 -  level type \commdx{kill}). After the parent theory has
    1.21 -  been modified, you go back to your original theory. When its first line
    1.22 -  \isa{\isacommand{theory}~T~=~\dots~:} is processed, the
    1.23 +  \indexbold{abandoning a theory}\indexbold{theories!abandoning} (at the
    1.24 +  shell level type \commdx{kill}). After the parent theory has been modified,
    1.25 +  you go back to your original theory. When its opening
    1.26 +  \isacommand{theory}~\isa{T} \dots \isacommand{begin} is processed, the
    1.27    modified parent is reloaded automatically.
    1.28    
    1.29  %  The only time when you need to load a theory by hand is when you simply