# HG changeset patch
# User wenzelm
# Date 1212442707 -7200
# Node ID a53dfe9096748898c5251981580a88e37c453af9
# Parent  cd8d99b9ef099c49dcde92eeee3f57e25d975f27
moved header command to Document_Preparation;

diff -r cd8d99b9ef09 -r a53dfe909674 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Mon Jun 02 23:38:25 2008 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Mon Jun 02 23:38:27 2008 +0200
@@ -10,7 +10,6 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def "header"} & : & \isarkeep{toplevel} \\
     @{command_def "theory"} & : & \isartrans{toplevel}{theory} \\
     @{command_def (global) "end"} & : & \isartrans{theory}{toplevel} \\
   \end{matharray}
@@ -26,14 +25,11 @@
   ones.  Just preceding the @{command "theory"} keyword, there may be
   an optional @{command "header"} declaration, which is relevant to
   document preparation only; it acts very much like a special
-  pre-theory markup command (cf.\ \secref{sec:markup} and).  The
-  @{command (global) "end"} command
-  concludes a theory development; it has to be the very last command
-  of any theory file loaded in batch-mode.
+  pre-theory markup command (cf.\ \secref{sec:markup}).  The @{command
+  (global) "end"} command concludes a theory development; it has to be
+  the very last command of any theory file loaded in batch-mode.
 
   \begin{rail}
-    'header' text
-    ;
     'theory' name 'imports' (name +) uses? 'begin'
     ;
 
@@ -42,12 +38,6 @@
 
   \begin{descr}
 
-  \item [@{command "header"}~@{text "text"}] provides plain text
-  markup just preceding the formal beginning of a theory.  In actual
-  document preparation the corresponding {\LaTeX} macro @{verbatim
-  "\\isamarkupheader"} may be redefined to produce chapter or section
-  headings.  See also \secref{sec:markup} for further markup commands.
-  
   \item [@{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots>
   B\<^sub>n \<BEGIN>"}] starts a new theory @{text A} based on the
   merge of existing theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}.
@@ -102,9 +92,9 @@
   
   \item [@{command "context"}~@{text "c \<BEGIN>"}] recommences an
   existing locale or class context @{text c}.  Note that locale and
-  class definitions allow to include the @{keyword_ref "begin"}
-  keyword as well, in order to continue the local theory immediately
-  after the initial specification.
+  class definitions allow to include the @{keyword "begin"} keyword as
+  well, in order to continue the local theory immediately after the
+  initial specification.
   
   \item [@{command (local) "end"}] concludes the current local theory
   and continues the enclosing global theory.  Note that a global