# HG changeset patch
# User wenzelm
# Date 1008960939 -3600
# Node ID b85acd66f715b665d5475ad927841ecf6352d723
# Parent  dceea9dbdeddb7031e54ab7b9bac9f4df977c384
removed Misc/Translations (text covered by Documents.thy);

diff -r dceea9dbdedd -r b85acd66f715 doc-src/TutorialI/IsaMakefile
--- 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
diff -r dceea9dbdedd -r b85acd66f715 doc-src/TutorialI/Misc/ROOT.ML
--- 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";
diff -r dceea9dbdedd -r b85acd66f715 doc-src/TutorialI/Misc/Translations.thy
--- 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
-(*>*)
diff -r dceea9dbdedd -r b85acd66f715 doc-src/TutorialI/Misc/document/Translations.tex
--- 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:
diff -r dceea9dbdedd -r b85acd66f715 doc-src/TutorialI/Misc/simp.thy
--- 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,
diff -r dceea9dbdedd -r b85acd66f715 doc-src/TutorialI/fp.tex
--- 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}