*** empty log message ***

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

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