--- 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
-(*>*)