# HG changeset patch
# User wenzelm
# Date 1117963878 -7200
# Node ID 56e56a00511e6aa6f30a1bbb13e9cefe45a5544c
# Parent  1b2683e18fd28e7460b842e7d9543e92a1e82e8d
updated theory header syntax;

diff -r 1b2683e18fd2 -r 56e56a00511e doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Sun Jun 05 11:31:17 2005 +0200
+++ b/doc-src/IsarRef/pure.tex	Sun Jun 05 11:31:18 2005 +0200
@@ -50,12 +50,12 @@
 \begin{rail}
   'header' text
   ;
-  'theory' name '=' (name + '+') filespecs? ':'
+  'theory' name 'imports' (name +) uses? 'begin'
   ;
   'context' name
   ;
 
-  filespecs: 'files' ((name | parname) +);
+  uses: 'uses' ((name | parname) +);
 \end{rail}
 
 \begin{descr}
@@ -65,8 +65,9 @@
   produce chapter or section headings.  See also \S\ref{sec:markup-thy} and
   \S\ref{sec:markup-prf} for further markup commands.
   
-\item [$\THEORY~A = B@1 + \cdots + B@n\colon$] starts a new theory $A$ based
-  on the merge of existing theories $B@1, \dots, B@n$.
+\item [$\THEORY~A~\isarkeyword{imports}~B@1~\ldots~B@n~\isarkeyword{begin}$]
+  starts a new theory $A$ based on the merge of existing theories $B@1, \dots,
+  B@n$.
   
   Due to inclusion of several ancestors, the overall theory structure emerging
   in an Isabelle session forms a directed acyclic graph (DAG).  Isabelle's
@@ -75,7 +76,7 @@
   processing theory headers interactively; batch-mode explicitly distinguishes
   \verb,update_thy, from \verb,use_thy,, see also \cite{isabelle-ref}.
   
-  The optional $\isarkeyword{files}$ specification declares additional
+  The optional $\isarkeyword{uses}$ specification declares additional
   dependencies on ML files.  Files will be loaded immediately, unless the name
   is put in parentheses, which merely documents the dependency to be resolved
   later in the text (typically via explicit $\isarcmd{use}$ in the body text,