--- a/doc-src/TutorialI/IsaMakefile Mon Mar 12 18:23:11 2001 +0100
+++ b/doc-src/TutorialI/IsaMakefile Tue Mar 13 18:35:48 2001 +0100
@@ -164,7 +164,7 @@
$(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/Option2.thy \
- Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \
+ Misc/types.thy Misc/prime_def.thy Misc/Translations.thy Misc/case_exprs.thy \
Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy
$(USEDIR) Misc
@rm -f tutorial.dvi
--- a/doc-src/TutorialI/Misc/ROOT.ML Mon Mar 12 18:23:11 2001 +0100
+++ b/doc-src/TutorialI/Misc/ROOT.ML Tue Mar 13 18:35:48 2001 +0100
@@ -8,6 +8,7 @@
use_thy "Option2";
use_thy "types";
use_thy "prime_def";
+use_thy "Translations";
use_thy "simp";
use_thy "Itrev";
use_thy "AdvancedInd";
--- a/doc-src/TutorialI/Sets/sets.tex Mon Mar 12 18:23:11 2001 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex Tue Mar 13 18:35:48 2001 +0100
@@ -323,18 +323,17 @@
\rulename{UN_E}
\end{isabelle}
%
-The following built-in abbreviation lets us express the union
-over a \emph{type}:
+The following built-in syntax translation (see \S\ref{sec:def-translations})
+lets us express the union over a \emph{type}:
\begin{isabelle}
\ \ \ \ \
({\isasymUnion}x.\ B\ x)\ {\isasymrightleftharpoons}\
({\isasymUnion}x{\isasymin}UNIV.\ B\ x)
\end{isabelle}
-Abbreviations work as you might expect. The term on the left-hand side of
-the
-\indexboldpos{\isasymrightleftharpoons}{$IsaEqq} symbol is automatically translated to the right-hand side when the
-term is parsed, the reverse translation being done when the term is
-displayed.
+%Abbreviations work as you might expect. The term on the left-hand side of
+%the \isasymrightleftharpoons\ symbol is automatically translated to the right-hand side when the
+%term is parsed, the reverse translation being done when the term is
+%displayed.
We may also express the union of a set of sets, written \isa{Union\ C} in
\textsc{ascii}:
@@ -426,10 +425,10 @@
$\binom{n}{k}$.
\begin{warn}
-The term \isa{Finite\ A} is an abbreviation for
-\isa{A\ \isasymin\ Finites}, where the constant \isa{Finites} denotes the
-set of all finite sets of a given type. There is no constant
-\isa{Finite}.
+The term \isa{finite\ A} is defined via a syntax translation as an
+abbreviation for \isa{A \isasymin Finites}, where the constant \isa{Finites}
+denotes the set of all finite sets of a given type. There is no constant
+\isa{finite}.
\end{warn}
\index{sets|)}
@@ -1077,4 +1076,4 @@
two agents in a process algebra is an example of coinduction.
The coinduction rule can be strengthened in various ways; see
theory \isa{Gfp} for details.
-\index{fixed points|)}
\ No newline at end of file
+\index{fixed points|)}
--- a/doc-src/TutorialI/appendix.tex Mon Mar 12 18:23:11 2001 +0100
+++ b/doc-src/TutorialI/appendix.tex Tue Mar 13 18:35:48 2001 +0100
@@ -22,6 +22,15 @@
\indexboldpos{\isasymequiv}{$IsaEq} &
\ttindexboldpos{==}{$IsaEq} &
\verb$\<equiv>$ \\
+\indexboldpos{\isasymrightleftharpoons}{$IsaEqTrans} &
+\ttindexboldpos{==}{$IsaEq} &
+\verb$\<rightleftharpoons>$ \\
+\indexboldpos{\isasymrightharpoonup}{$IsaEqTrans1} &
+\ttindexboldpos{=>}{$IsaFun} &
+\verb$\<rightharpoonup>$ \\
+\indexboldpos{\isasymleftharpoondown}{$IsaEqTrans2} &
+\ttindexboldpos{<=}{$IsaFun2} &
+\verb$\<leftharpoondown>$ \\
\indexboldpos{\isasymlambda}{$Isalam} &
\texttt{\%}\indexbold{$Isalam@\texttt{\%}} &
\verb$\<lambda>$ \\
--- a/doc-src/TutorialI/fp.tex Mon Mar 12 18:23:11 2001 +0100
+++ b/doc-src/TutorialI/fp.tex Tue Mar 13 18:35:48 2001 +0100
@@ -268,6 +268,8 @@
\input{Misc/document/prime_def.tex}
+\input{Misc/document/Translations.tex}
+
\section{The Definitional Approach}
\label{sec:definitional}
@@ -288,6 +290,8 @@
as pure \isacommand{defs} are, but more convenient. And this is not just the
case for \isacommand{primrec} but also for the other commands described
later, like \isacommand{recdef} and \isacommand{inductive}.
+This strict adherence to the definitional approach reduces the risk of
+soundness errors inside Isabelle/HOL.
\chapter{More Functional Programming}
--- a/doc-src/TutorialI/todo.tobias Mon Mar 12 18:23:11 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias Tue Mar 13 18:35:48 2001 +0100
@@ -61,14 +61,13 @@
differences between our HOL and the other one.
Syntax translations! Harpoons already used!
+say something about "abbreviations" when defs are introduced.
warning: simp of asms from l to r; may require reordering (rotate_tac)
Adjust FP textbook refs: new Bird, Hudak
Discrete math textbook: Rosen?
-say something about "abbreviations" when defs are introduced.
-
adjust type of ^ in tab:overloading
an example of induction: !y. A --> B --> C ??