# HG changeset patch
# User nipkow
# Date 984504948 -3600
# Node ID 881222d487778b407f846b0d1929a4f700c9c125
# Parent  f8da11ca4c6e8abe310286ffba571398c405858b
*** empty log message ***

diff -r f8da11ca4c6e -r 881222d48777 doc-src/TutorialI/IsaMakefile
--- 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
diff -r f8da11ca4c6e -r 881222d48777 doc-src/TutorialI/Misc/ROOT.ML
--- 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";
diff -r f8da11ca4c6e -r 881222d48777 doc-src/TutorialI/Sets/sets.tex
--- 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|)}
diff -r f8da11ca4c6e -r 881222d48777 doc-src/TutorialI/appendix.tex
--- 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>$ \\
diff -r f8da11ca4c6e -r 881222d48777 doc-src/TutorialI/fp.tex
--- 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}
 
diff -r f8da11ca4c6e -r 881222d48777 doc-src/TutorialI/todo.tobias
--- 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 ??