1.1 --- a/doc-src/TutorialI/IsaMakefile Wed Nov 29 18:42:40 2000 +0100
1.2 +++ b/doc-src/TutorialI/IsaMakefile Thu Nov 30 13:56:46 2000 +0100
1.3 @@ -78,7 +78,7 @@
1.4
1.5 HOL-Trie: HOL $(LOG)/HOL-Trie.gz
1.6
1.7 -$(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/Option2.thy Trie/Trie.thy
1.8 +$(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy
1.9 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Trie
1.10 @rm -f tutorial.dvi
1.11
1.12 @@ -154,8 +154,8 @@
1.13 HOL-Misc: HOL $(LOG)/HOL-Misc.gz
1.14
1.15 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
1.16 - Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy \
1.17 - Misc/prime_def.thy Misc/case_exprs.thy \
1.18 + Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/Option2.thy \
1.19 + Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \
1.20 Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy
1.21 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Misc
1.22 @rm -f tutorial.dvi
2.1 --- a/doc-src/TutorialI/Misc/ROOT.ML Wed Nov 29 18:42:40 2000 +0100
2.2 +++ b/doc-src/TutorialI/Misc/ROOT.ML Thu Nov 30 13:56:46 2000 +0100
2.3 @@ -5,6 +5,7 @@
2.4 use_thy "fakenat";
2.5 use_thy "natsum";
2.6 use_thy "pairs";
2.7 +use_thy "Option2";
2.8 use_thy "types";
2.9 use_thy "prime_def";
2.10 use_thy "simp";
3.1 --- a/doc-src/TutorialI/Misc/document/pairs.tex Wed Nov 29 18:42:40 2000 +0100
3.2 +++ b/doc-src/TutorialI/Misc/document/pairs.tex Thu Nov 30 13:56:46 2000 +0100
3.3 @@ -3,8 +3,7 @@
3.4 \def\isabellecontext{pairs}%
3.5 %
3.6 \begin{isamarkuptext}%
3.7 -\label{sec:pairs}\indexbold{product type}
3.8 -\index{pair|see{product type}}\index{tuple|see{product type}}
3.9 +\label{sec:pairs}\indexbold{pair}
3.10 HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
3.11 \indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type
3.12 $\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and
4.1 --- a/doc-src/TutorialI/Misc/pairs.thy Wed Nov 29 18:42:40 2000 +0100
4.2 +++ b/doc-src/TutorialI/Misc/pairs.thy Thu Nov 30 13:56:46 2000 +0100
4.3 @@ -1,8 +1,7 @@
4.4 (*<*)
4.5 theory pairs = Main:;
4.6 (*>*)
4.7 -text{*\label{sec:pairs}\indexbold{product type}
4.8 -\index{pair|see{product type}}\index{tuple|see{product type}}
4.9 +text{*\label{sec:pairs}\indexbold{pair}
4.10 HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
4.11 \indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type
4.12 $\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and
5.1 --- a/doc-src/TutorialI/Trie/Option2.thy Wed Nov 29 18:42:40 2000 +0100
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,8 +0,0 @@
5.4 -(*<*)
5.5 -theory Option2 = Main:;
5.6 -(*>*)
5.7 -
5.8 -datatype 'a option = None | Some 'a;
5.9 -(*<*)
5.10 -end
5.11 -(*>*)
6.1 --- a/doc-src/TutorialI/Trie/ROOT.ML Wed Nov 29 18:42:40 2000 +0100
6.2 +++ b/doc-src/TutorialI/Trie/ROOT.ML Thu Nov 30 13:56:46 2000 +0100
6.3 @@ -1,3 +1,2 @@
6.4 use "../settings.ML";
6.5 -use_thy "Option2";
6.6 use_thy "Trie";
7.1 --- a/doc-src/TutorialI/Trie/document/Option2.tex Wed Nov 29 18:42:40 2000 +0100
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,9 +0,0 @@
7.4 -%
7.5 -\begin{isabellebody}%
7.6 -\def\isabellecontext{Option{\isadigit{2}}}%
7.7 -\isanewline
7.8 -\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabellebody}%
7.9 -%%% Local Variables:
7.10 -%%% mode: latex
7.11 -%%% TeX-master: "root"
7.12 -%%% End:
8.1 --- a/doc-src/TutorialI/Types/types.tex Wed Nov 29 18:42:40 2000 +0100
8.2 +++ b/doc-src/TutorialI/Types/types.tex Thu Nov 30 13:56:46 2000 +0100
8.3 @@ -19,11 +19,9 @@
8.4 \section{Numbers}
8.5 \label{sec:numbers}
8.6
8.7 -\index{product type|(}
8.8 +\index{pair|(}
8.9 \input{Types/document/Pairs}
8.10 -\index{product type|)}
8.11 -% Check refs to this section to see what is expected of it.
8.12 -% Mention type unit
8.13 +\index{pair|)}
8.14
8.15 \section{Records}
8.16 \label{sec:records}
9.1 --- a/doc-src/TutorialI/fp.tex Wed Nov 29 18:42:40 2000 +0100
9.2 +++ b/doc-src/TutorialI/fp.tex Thu Nov 30 13:56:46 2000 +0100
9.3 @@ -244,6 +244,10 @@
9.4 \subsection{Pairs}
9.5 \input{Misc/document/pairs.tex}
9.6
9.7 +\subsection{Datatype \emph{\texttt{option}}}
9.8 +\label{sec:option}
9.9 +\input{Misc/document/Option2.tex}
9.10 +
9.11 \section{Definitions}
9.12 \label{sec:Definitions}
9.13
9.14 @@ -388,6 +392,7 @@
9.15 \index{*datatype|)}
9.16
9.17 \subsection{Case study: Tries}
9.18 +\label{sec:Trie}
9.19
9.20 Tries are a classic search tree data structure~\cite{Knuth3-75} for fast
9.21 indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a
9.22 @@ -436,12 +441,8 @@
9.23
9.24 Proper tries associate some value with each string. Since the
9.25 information is stored only in the final node associated with the string, many
9.26 -nodes do not carry any value. This distinction is captured by the
9.27 -following predefined datatype (from theory \isa{Option}, which is a parent
9.28 -of \isa{Main}):
9.29 -\smallskip
9.30 -\input{Trie/document/Option2.tex}
9.31 -\indexbold{*option}\indexbold{*None}\indexbold{*Some}%
9.32 +nodes do not carry any value. This distinction is modeled with the help
9.33 +of the predefined datatype \isa{option} (see {\S}\ref{sec:option}).
9.34 \input{Trie/document/Trie.tex}
9.35
9.36 \begin{exercise}
10.1 --- a/doc-src/TutorialI/tutorial.tex Wed Nov 29 18:42:40 2000 +0100
10.2 +++ b/doc-src/TutorialI/tutorial.tex Thu Nov 30 13:56:46 2000 +0100
10.3 @@ -45,6 +45,9 @@
10.4 \newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}
10.5 \newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}
10.6
10.7 +\index{product type|see{pair}}
10.8 +\index{tuple|see{pair}}
10.9 +
10.10 \underscoreoff
10.11
10.12 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???