# HG changeset patch
# User nipkow
# Date 1092678421 -7200
# Node ID 1275417e3930be4b1d8092a720b3b5f191052f08
# Parent  f00857c7539b566865ea5e515c978fa2c8fd11ce
Adapted text to new theory header syntax.

diff -r f00857c7539b -r 1275417e3930 doc-src/TutorialI/Documents/Documents.thy
--- a/doc-src/TutorialI/Documents/Documents.thy	Mon Aug 16 19:06:59 2004 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy	Mon Aug 16 19:47:01 2004 +0200
@@ -489,7 +489,9 @@
   \begin{ttbox}
   header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
 
-  theory Foo_Bar = Main:
+  theory Foo_Bar
+  import Main
+  begin
 
   subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
 
@@ -764,7 +766,9 @@
 
   \begin{tabular}{l}
   \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
-  \texttt{theory T = Main:} \\
+  \texttt{theory T} \\
+  \texttt{import Main} \\
+  \texttt{begin} \\
   \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
   ~~$\vdots$ \\
   \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
@@ -796,11 +800,13 @@
   easy to invalidate the visible text by hiding references to
   questionable axioms.
 
-  Authentic reports of Isabelle/Isar theories, say as part of a
-  library, should suppress nothing.  Other users may need the full
-  information for their own derivative work.  If a particular
-  formalization appears inadequate for general public coverage, it is
-  often more appropriate to think of a better way in the first place.
+% I removed this because the page overflowed and I disagree a little. TN
+%
+%  Authentic reports of Isabelle/Isar theories, say as part of a
+% library, should suppress nothing.  Other users may need the full
+% information for their own derivative work.  If a particular
+% formalization appears inadequate for general public coverage, it is
+% often more appropriate to think of a better way in the first place.
 
   \medskip Some technical subtleties of the
   \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
diff -r f00857c7539b -r 1275417e3930 doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Mon Aug 16 19:06:59 2004 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Mon Aug 16 19:47:01 2004 +0200
@@ -503,7 +503,9 @@
   \begin{ttbox}
   header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
 
-  theory Foo_Bar = Main:
+  theory Foo_Bar
+  import Main
+  begin
 
   subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
 
@@ -793,7 +795,9 @@
 
   \begin{tabular}{l}
   \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
-  \texttt{theory T = Main:} \\
+  \texttt{theory T} \\
+  \texttt{import Main} \\
+  \texttt{begin} \\
   \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
   ~~$\vdots$ \\
   \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
@@ -826,11 +830,13 @@
   easy to invalidate the visible text by hiding references to
   questionable axioms.
 
-  Authentic reports of Isabelle/Isar theories, say as part of a
-  library, should suppress nothing.  Other users may need the full
-  information for their own derivative work.  If a particular
-  formalization appears inadequate for general public coverage, it is
-  often more appropriate to think of a better way in the first place.
+% I removed this because the page overflowed and I disagree a little. TN
+%
+%  Authentic reports of Isabelle/Isar theories, say as part of a
+% library, should suppress nothing.  Other users may need the full
+% information for their own derivative work.  If a particular
+% formalization appears inadequate for general public coverage, it is
+% often more appropriate to think of a better way in the first place.
 
   \medskip Some technical subtleties of the
   \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
diff -r f00857c7539b -r 1275417e3930 doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Mon Aug 16 19:06:59 2004 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Mon Aug 16 19:47:01 2004 +0200
@@ -1,4 +1,6 @@
-theory ToyList = PreList:
+theory ToyList
+import PreList
+begin
 
 text{*\noindent
 HOL already has a predefined theory of lists called @{text"List"} ---
diff -r f00857c7539b -r 1275417e3930 doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Aug 16 19:06:59 2004 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Aug 16 19:47:01 2004 +0200
@@ -1,7 +1,9 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{ToyList}%
-\isacommand{theory}\ ToyList\ {\isacharequal}\ PreList{\isacharcolon}\isamarkupfalse%
+\isacommand{theory}\ ToyList\isanewline
+\isakeyword{import}\ PreList\isanewline
+\isakeyword{begin}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
diff -r f00857c7539b -r 1275417e3930 doc-src/TutorialI/ToyList2/ToyList1
--- a/doc-src/TutorialI/ToyList2/ToyList1	Mon Aug 16 19:06:59 2004 +0200
+++ b/doc-src/TutorialI/ToyList2/ToyList1	Mon Aug 16 19:47:01 2004 +0200
@@ -1,4 +1,6 @@
-theory ToyList = PreList:
+theory ToyList
+import PreList
+begin
 
 datatype 'a list = Nil                          ("[]")
                  | Cons 'a "'a list"            (infixr "#" 65)
diff -r f00857c7539b -r 1275417e3930 doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Mon Aug 16 19:06:59 2004 +0200
+++ b/doc-src/TutorialI/basics.tex	Mon Aug 16 19:47:01 2004 +0200
@@ -52,11 +52,13 @@
 specification language. In fact, theories in HOL can be either. The general
 format of a theory \texttt{T} is
 \begin{ttbox}
-theory T = B\(@1\) + \(\cdots\) + B\(@n\):
+theory T
+import B\(@1\) \(\ldots\) B\(@n\)
+begin
 {\rmfamily\textit{declarations, definitions, and proofs}}
 end
 \end{ttbox}
-where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
+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
 (types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the