1.1 --- a/doc-src/TutorialI/Documents/Documents.thy Mon Aug 16 19:06:59 2004 +0200
1.2 +++ b/doc-src/TutorialI/Documents/Documents.thy Mon Aug 16 19:47:01 2004 +0200
1.3 @@ -489,7 +489,9 @@
1.4 \begin{ttbox}
1.5 header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
1.6
1.7 - theory Foo_Bar = Main:
1.8 + theory Foo_Bar
1.9 + import Main
1.10 + begin
1.11
1.12 subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
1.13
1.14 @@ -764,7 +766,9 @@
1.15
1.16 \begin{tabular}{l}
1.17 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
1.18 - \texttt{theory T = Main:} \\
1.19 + \texttt{theory T} \\
1.20 + \texttt{import Main} \\
1.21 + \texttt{begin} \\
1.22 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
1.23 ~~$\vdots$ \\
1.24 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
1.25 @@ -796,11 +800,13 @@
1.26 easy to invalidate the visible text by hiding references to
1.27 questionable axioms.
1.28
1.29 - Authentic reports of Isabelle/Isar theories, say as part of a
1.30 - library, should suppress nothing. Other users may need the full
1.31 - information for their own derivative work. If a particular
1.32 - formalization appears inadequate for general public coverage, it is
1.33 - often more appropriate to think of a better way in the first place.
1.34 +% I removed this because the page overflowed and I disagree a little. TN
1.35 +%
1.36 +% Authentic reports of Isabelle/Isar theories, say as part of a
1.37 +% library, should suppress nothing. Other users may need the full
1.38 +% information for their own derivative work. If a particular
1.39 +% formalization appears inadequate for general public coverage, it is
1.40 +% often more appropriate to think of a better way in the first place.
1.41
1.42 \medskip Some technical subtleties of the
1.43 \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
2.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex Mon Aug 16 19:06:59 2004 +0200
2.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Mon Aug 16 19:47:01 2004 +0200
2.3 @@ -503,7 +503,9 @@
2.4 \begin{ttbox}
2.5 header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
2.6
2.7 - theory Foo_Bar = Main:
2.8 + theory Foo_Bar
2.9 + import Main
2.10 + begin
2.11
2.12 subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
2.13
2.14 @@ -793,7 +795,9 @@
2.15
2.16 \begin{tabular}{l}
2.17 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
2.18 - \texttt{theory T = Main:} \\
2.19 + \texttt{theory T} \\
2.20 + \texttt{import Main} \\
2.21 + \texttt{begin} \\
2.22 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
2.23 ~~$\vdots$ \\
2.24 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
2.25 @@ -826,11 +830,13 @@
2.26 easy to invalidate the visible text by hiding references to
2.27 questionable axioms.
2.28
2.29 - Authentic reports of Isabelle/Isar theories, say as part of a
2.30 - library, should suppress nothing. Other users may need the full
2.31 - information for their own derivative work. If a particular
2.32 - formalization appears inadequate for general public coverage, it is
2.33 - often more appropriate to think of a better way in the first place.
2.34 +% I removed this because the page overflowed and I disagree a little. TN
2.35 +%
2.36 +% Authentic reports of Isabelle/Isar theories, say as part of a
2.37 +% library, should suppress nothing. Other users may need the full
2.38 +% information for their own derivative work. If a particular
2.39 +% formalization appears inadequate for general public coverage, it is
2.40 +% often more appropriate to think of a better way in the first place.
2.41
2.42 \medskip Some technical subtleties of the
2.43 \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
3.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy Mon Aug 16 19:06:59 2004 +0200
3.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy Mon Aug 16 19:47:01 2004 +0200
3.3 @@ -1,4 +1,6 @@
3.4 -theory ToyList = PreList:
3.5 +theory ToyList
3.6 +import PreList
3.7 +begin
3.8
3.9 text{*\noindent
3.10 HOL already has a predefined theory of lists called @{text"List"} ---
4.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Aug 16 19:06:59 2004 +0200
4.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Aug 16 19:47:01 2004 +0200
4.3 @@ -1,7 +1,9 @@
4.4 %
4.5 \begin{isabellebody}%
4.6 \def\isabellecontext{ToyList}%
4.7 -\isacommand{theory}\ ToyList\ {\isacharequal}\ PreList{\isacharcolon}\isamarkupfalse%
4.8 +\isacommand{theory}\ ToyList\isanewline
4.9 +\isakeyword{import}\ PreList\isanewline
4.10 +\isakeyword{begin}\isamarkupfalse%
4.11 %
4.12 \begin{isamarkuptext}%
4.13 \noindent
5.1 --- a/doc-src/TutorialI/ToyList2/ToyList1 Mon Aug 16 19:06:59 2004 +0200
5.2 +++ b/doc-src/TutorialI/ToyList2/ToyList1 Mon Aug 16 19:47:01 2004 +0200
5.3 @@ -1,4 +1,6 @@
5.4 -theory ToyList = PreList:
5.5 +theory ToyList
5.6 +import PreList
5.7 +begin
5.8
5.9 datatype 'a list = Nil ("[]")
5.10 | Cons 'a "'a list" (infixr "#" 65)
6.1 --- a/doc-src/TutorialI/basics.tex Mon Aug 16 19:06:59 2004 +0200
6.2 +++ b/doc-src/TutorialI/basics.tex Mon Aug 16 19:47:01 2004 +0200
6.3 @@ -52,11 +52,13 @@
6.4 specification language. In fact, theories in HOL can be either. The general
6.5 format of a theory \texttt{T} is
6.6 \begin{ttbox}
6.7 -theory T = B\(@1\) + \(\cdots\) + B\(@n\):
6.8 +theory T
6.9 +import B\(@1\) \(\ldots\) B\(@n\)
6.10 +begin
6.11 {\rmfamily\textit{declarations, definitions, and proofs}}
6.12 end
6.13 \end{ttbox}
6.14 -where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
6.15 +where \texttt{B}$@1$ \dots\ \texttt{B}$@n$ are the names of existing
6.16 theories that \texttt{T} is based on and \textit{declarations,
6.17 definitions, and proofs} represents the newly introduced concepts
6.18 (types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the