--- a/doc-src/TutorialI/IsaMakefile Fri Dec 21 17:31:45 2001 +0100
+++ b/doc-src/TutorialI/IsaMakefile Fri Dec 21 19:55:39 2001 +0100
@@ -169,7 +169,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/Translations.thy Misc/case_exprs.thy \
+ Misc/types.thy Misc/prime_def.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 Fri Dec 21 17:31:45 2001 +0100
+++ b/doc-src/TutorialI/Misc/ROOT.ML Fri Dec 21 19:55:39 2001 +0100
@@ -8,7 +8,6 @@
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/Misc/Translations.thy Fri Dec 21 17:31:45 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(*<*)
-theory Translations = Main:
-(*>*)
-subsection{*Syntax Translations*}
-
-text{*\label{sec:def-translations}
-\index{syntax translations|(}%
-\index{translations@\isacommand {translations} (command)|(}
-Isabelle offers an additional definitional facility,
-\textbf{syntax translations}.
-They resemble macros: upon parsing, the defined concept is immediately
-replaced by its definition. This effect is reversed upon printing. For example,
-the symbol @{text"\<noteq>"} is defined via a syntax translation:
-*}
-
-translations "x \<noteq> y" \<rightleftharpoons> "\<not>(x = y)"
-
-text{*\index{$IsaEqTrans@\isasymrightleftharpoons}
-\noindent
-Internally, @{text"\<noteq>"} never appears.
-
-In addition to @{text"\<rightleftharpoons>"} there are
-@{text"\<rightharpoonup>"}\index{$IsaEqTrans1@\isasymrightharpoonup}
-and @{text"\<leftharpoondown>"}\index{$IsaEqTrans2@\isasymleftharpoondown}
-for uni-directional translations, which only affect
-parsing or printing. This tutorial will not cover the details of
-translations. We have mentioned the concept merely because it
-crops up occasionally; a number of HOL's built-in constructs are defined
-via translations. Translations are preferable to definitions when the new
-concept is a trivial variation on an existing one. For example, we
-don't need to derive new theorems about @{text"\<noteq>"}, since existing theorems
-about @{text"="} still apply.%
-\index{syntax translations|)}%
-\index{translations@\isacommand {translations} (command)|)}
-*}
-
-(*<*)
-end
-(*>*)
--- a/doc-src/TutorialI/Misc/document/Translations.tex Fri Dec 21 17:31:45 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Translations}%
-\isamarkupfalse%
-%
-\isamarkupsubsection{Syntax Translations%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\label{sec:def-translations}
-\index{syntax translations|(}%
-\index{translations@\isacommand {translations} (command)|(}
-Isabelle offers an additional definitional facility,
-\textbf{syntax translations}.
-They resemble macros: upon parsing, the defined concept is immediately
-replaced by its definition. This effect is reversed upon printing. For example,
-the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-\index{$IsaEqTrans@\isasymrightleftharpoons}
-\noindent
-Internally, \isa{{\isasymnoteq}} never appears.
-
-In addition to \isa{{\isasymrightleftharpoons}} there are
-\isa{{\isasymrightharpoonup}}\index{$IsaEqTrans1@\isasymrightharpoonup}
-and \isa{{\isasymleftharpoondown}}\index{$IsaEqTrans2@\isasymleftharpoondown}
-for uni-directional translations, which only affect
-parsing or printing. This tutorial will not cover the details of
-translations. We have mentioned the concept merely because it
-crops up occasionally; a number of HOL's built-in constructs are defined
-via translations. Translations are preferable to definitions when the new
-concept is a trivial variation on an existing one. For example, we
-don't need to derive new theorems about \isa{{\isasymnoteq}}, since existing theorems
-about \isa{{\isacharequal}} still apply.%
-\index{syntax translations|)}%
-\index{translations@\isacommand {translations} (command)|)}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isamarkupfalse%
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/TutorialI/Misc/simp.thy Fri Dec 21 17:31:45 2001 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy Fri Dec 21 19:55:39 2001 +0100
@@ -156,8 +156,7 @@
Constant definitions (\S\ref{sec:ConstDefinitions}) can be used as
simplification rules, but by default they are not: the simplifier does not
expand them automatically. Definitions are intended for introducing abstract
-concepts and not merely as abbreviations. (Contrast with syntax
-translations, \S\ref{sec:def-translations}.) Of course, we need to expand
+concepts and not merely as abbreviations. Of course, we need to expand
the definition initially, but once we have proved enough abstract properties
of the new constant, we can forget its original definition. This style makes
proofs more robust: if the definition has to be changed,
--- a/doc-src/TutorialI/fp.tex Fri Dec 21 17:31:45 2001 +0100
+++ b/doc-src/TutorialI/fp.tex Fri Dec 21 19:55:39 2001 +0100
@@ -297,8 +297,6 @@
\input{Misc/document/prime_def.tex}
-\input{Misc/document/Translations.tex}
-
\section{The Definitional Approach}
\label{sec:definitional}