--- a/doc-src/IsarRef/Thy/Spec.thy Fri May 09 23:35:57 2008 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Sat May 10 00:14:00 2008 +0200
@@ -6,4 +6,69 @@
chapter {* Specifications *}
+section {* Defining theories \label{sec:begin-thy} *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "header"} & : & \isarkeep{toplevel} \\
+ @{command_def "theory"} & : & \isartrans{toplevel}{theory} \\
+ @{command_def "end"} & : & \isartrans{theory}{toplevel} \\
+ \end{matharray}
+
+ Isabelle/Isar theories are defined via theory, which contain both
+ specifications and proofs; occasionally definitional mechanisms also
+ require some explicit proof.
+
+ The first ``real'' command of any theory has to be @{command
+ "theory"}, which starts a new theory based on the merge of existing
+ 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-thy} and
+ \secref{sec:markup-thy}). The @{command "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'
+ ;
+
+ uses: 'uses' ((name | parname) +);
+ \end{rail}
+
+ \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-thy} and
+ \secref{sec:markup-prf} 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"}.
+
+ Due to inclusion of several ancestors, the overall theory structure
+ emerging in an Isabelle session forms a directed acyclic graph
+ (DAG). Isabelle's theory loader ensures that the sources
+ contributing to the development graph are always up-to-date.
+ Changed files are automatically reloaded when processing theory
+ headers.
+
+ The optional @{keyword_def "uses"} specification declares additional
+ dependencies on extra files (usually ML sources). Files will be
+ loaded immediately (as ML), unless the name is put in parentheses,
+ which merely documents the dependency to be resolved later in the
+ text (typically via explicit @{command_ref "use"} in the body text,
+ see \secref{sec:ML}).
+
+ \item [@{command "end"}] concludes the current theory definition or
+ context switch.
+
+ \end{descr}
+*}
+
end