# HG changeset patch
# User wenzelm
# Date 1142350172 -3600
# Node ID a49c0f7c96340da215571a350566d1c96297ace0
# Parent  e80e3fdda60665a99c2c5179567c01f319aed5e4
tuned constdecl;
added 'no_translations';

diff -r e80e3fdda606 -r a49c0f7c9634 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Tue Mar 14 16:29:31 2006 +0100
+++ b/doc-src/IsarRef/pure.tex	Tue Mar 14 16:29:32 2006 +0100
@@ -257,7 +257,7 @@
 
   structs: '(' 'structure' (vars + 'and') ')'
   ;
-  constdecl: ((name '::' type) mixfix | (name '::' type)) 'where'? | name 'where'
+  constdecl:  ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
   ;
   constdef: thmdecl? prop
   ;
@@ -299,11 +299,13 @@
 
 \subsection{Syntax and translations}\label{sec:syn-trans}
 
-\indexisarcmd{syntax}\indexisarcmd{no-syntax}\indexisarcmd{translations}
+\indexisarcmd{syntax}\indexisarcmd{no-syntax}
+\indexisarcmd{translations}\indexisarcmd{no-translations}
 \begin{matharray}{rcl}
   \isarcmd{syntax} & : & \isartrans{theory}{theory} \\
   \isarcmd{no_syntax} & : & \isartrans{theory}{theory} \\
   \isarcmd{translations} & : & \isartrans{theory}{theory} \\
+  \isarcmd{no_translations} & : & \isartrans{theory}{theory} \\
 \end{matharray}
 
 \railalias{rightleftharpoons}{\isasymrightleftharpoons}
@@ -315,13 +317,10 @@
 \railalias{leftharpoondown}{\isasymleftharpoondown}
 \railterm{leftharpoondown}
 
-\railalias{nosyntax}{no\_syntax}
-\railterm{nosyntax}
-
 \begin{rail}
-  ('syntax' | nosyntax) mode? (constdecl +)
+  ('syntax' | 'no\_syntax') mode? (constdecl +)
   ;
-  'translations' (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
+  ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
   ;
 
   mode: ('(' ( name | 'output' | name 'output' ) ')')
@@ -349,6 +348,11 @@
   rules (\isasymrightharpoonup), or print rules (\isasymleftharpoondown).
   Translation patterns may be prefixed by the syntactic category to be used
   for parsing; the default is $logic$.
+  
+\item [$\isarkeyword{no_translations}~rules$] removes syntactic
+  translation rules, which are interpreted in the same manner as for
+  $\isarkeyword{translations}$ above.
+
 \end{descr}