# HG changeset patch
# User nipkow
# Date 975589006 -3600
# Node ID 8e4307d1207ae36a7226388ed93b3c23c4138702
# Parent  92cd56dfc17e78d8002d3e2a8fa624341b9d02a7
*** empty log message ***

diff -r 92cd56dfc17e -r 8e4307d1207a doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Wed Nov 29 18:42:40 2000 +0100
+++ b/doc-src/TutorialI/IsaMakefile	Thu Nov 30 13:56:46 2000 +0100
@@ -78,7 +78,7 @@
 
 HOL-Trie: HOL $(LOG)/HOL-Trie.gz
 
-$(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/Option2.thy Trie/Trie.thy
+$(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Trie
 	@rm -f tutorial.dvi
 
@@ -154,8 +154,8 @@
 HOL-Misc: HOL $(LOG)/HOL-Misc.gz
 
 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
-  Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy \
-  Misc/prime_def.thy Misc/case_exprs.thy \
+  Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/Option2.thy \
+  Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \
   Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Misc
 	@rm -f tutorial.dvi
diff -r 92cd56dfc17e -r 8e4307d1207a doc-src/TutorialI/Misc/ROOT.ML
--- a/doc-src/TutorialI/Misc/ROOT.ML	Wed Nov 29 18:42:40 2000 +0100
+++ b/doc-src/TutorialI/Misc/ROOT.ML	Thu Nov 30 13:56:46 2000 +0100
@@ -5,6 +5,7 @@
 use_thy "fakenat";
 use_thy "natsum";
 use_thy "pairs";
+use_thy "Option2";
 use_thy "types";
 use_thy "prime_def";
 use_thy "simp";
diff -r 92cd56dfc17e -r 8e4307d1207a doc-src/TutorialI/Misc/document/pairs.tex
--- a/doc-src/TutorialI/Misc/document/pairs.tex	Wed Nov 29 18:42:40 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/pairs.tex	Thu Nov 30 13:56:46 2000 +0100
@@ -3,8 +3,7 @@
 \def\isabellecontext{pairs}%
 %
 \begin{isamarkuptext}%
-\label{sec:pairs}\indexbold{product type}
-\index{pair|see{product type}}\index{tuple|see{product type}}
+\label{sec:pairs}\indexbold{pair}
 HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
 \indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type
 $\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and
diff -r 92cd56dfc17e -r 8e4307d1207a doc-src/TutorialI/Misc/pairs.thy
--- a/doc-src/TutorialI/Misc/pairs.thy	Wed Nov 29 18:42:40 2000 +0100
+++ b/doc-src/TutorialI/Misc/pairs.thy	Thu Nov 30 13:56:46 2000 +0100
@@ -1,8 +1,7 @@
 (*<*)
 theory pairs = Main:;
 (*>*)
-text{*\label{sec:pairs}\indexbold{product type}
-\index{pair|see{product type}}\index{tuple|see{product type}}
+text{*\label{sec:pairs}\indexbold{pair}
 HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
 \indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type
 $\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and
diff -r 92cd56dfc17e -r 8e4307d1207a doc-src/TutorialI/Trie/Option2.thy
--- a/doc-src/TutorialI/Trie/Option2.thy	Wed Nov 29 18:42:40 2000 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-(*<*)
-theory Option2 = Main:;
-(*>*)
-
-datatype 'a option = None | Some 'a;
-(*<*)
-end
-(*>*)
diff -r 92cd56dfc17e -r 8e4307d1207a doc-src/TutorialI/Trie/ROOT.ML
--- a/doc-src/TutorialI/Trie/ROOT.ML	Wed Nov 29 18:42:40 2000 +0100
+++ b/doc-src/TutorialI/Trie/ROOT.ML	Thu Nov 30 13:56:46 2000 +0100
@@ -1,3 +1,2 @@
 use "../settings.ML";
-use_thy "Option2";
 use_thy "Trie";
diff -r 92cd56dfc17e -r 8e4307d1207a doc-src/TutorialI/Trie/document/Option2.tex
--- a/doc-src/TutorialI/Trie/document/Option2.tex	Wed Nov 29 18:42:40 2000 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Option{\isadigit{2}}}%
-\isanewline
-\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
diff -r 92cd56dfc17e -r 8e4307d1207a doc-src/TutorialI/Types/types.tex
--- a/doc-src/TutorialI/Types/types.tex	Wed Nov 29 18:42:40 2000 +0100
+++ b/doc-src/TutorialI/Types/types.tex	Thu Nov 30 13:56:46 2000 +0100
@@ -19,11 +19,9 @@
 \section{Numbers}
 \label{sec:numbers}
 
-\index{product type|(}
+\index{pair|(}
 \input{Types/document/Pairs}
-\index{product type|)}
-% Check refs to this section to see what is expected of it.
-% Mention type unit
+\index{pair|)}
 
 \section{Records}
 \label{sec:records}
diff -r 92cd56dfc17e -r 8e4307d1207a doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Wed Nov 29 18:42:40 2000 +0100
+++ b/doc-src/TutorialI/fp.tex	Thu Nov 30 13:56:46 2000 +0100
@@ -244,6 +244,10 @@
 \subsection{Pairs}
 \input{Misc/document/pairs.tex}
 
+\subsection{Datatype \emph{\texttt{option}}}
+\label{sec:option}
+\input{Misc/document/Option2.tex}
+
 \section{Definitions}
 \label{sec:Definitions}
 
@@ -388,6 +392,7 @@
 \index{*datatype|)}
 
 \subsection{Case study: Tries}
+\label{sec:Trie}
 
 Tries are a classic search tree data structure~\cite{Knuth3-75} for fast
 indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a
@@ -436,12 +441,8 @@
 
 Proper tries associate some value with each string. Since the
 information is stored only in the final node associated with the string, many
-nodes do not carry any value. This distinction is captured by the
-following predefined datatype (from theory \isa{Option}, which is a parent
-of \isa{Main}):
-\smallskip
-\input{Trie/document/Option2.tex}
-\indexbold{*option}\indexbold{*None}\indexbold{*Some}%
+nodes do not carry any value. This distinction is modeled with the help
+of the predefined datatype \isa{option} (see {\S}\ref{sec:option}).
 \input{Trie/document/Trie.tex}
 
 \begin{exercise}
diff -r 92cd56dfc17e -r 8e4307d1207a doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Wed Nov 29 18:42:40 2000 +0100
+++ b/doc-src/TutorialI/tutorial.tex	Thu Nov 30 13:56:46 2000 +0100
@@ -45,6 +45,9 @@
 \newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}
 \newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}
 
+\index{product type|see{pair}}
+\index{tuple|see{pair}}
+
 \underscoreoff
 
 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???