doc-src/IsarRef/Thy/Inner_Syntax.thy

 
 section {* Syntax and translations \label{sec:syn-trans} *}
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def "nonterminals"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def "nonterminal"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "translations"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "no_translations"} & : & @{text "theory \<rightarrow> theory"} \\
   \end{matharray}
 
   \begin{rail}
-    'nonterminals' (name +)
+    'nonterminal' (name + 'and')
     ;
     ('syntax' | 'no_syntax') mode? (constdecl +)
     ;
     ('translations' | 'no_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
     ;

     ;
   \end{rail}
 
   \begin{description}
   
-  \item @{command "nonterminals"}~@{text c} declares a type
+  \item @{command "nonterminal"}~@{text c} declares a type
   constructor @{text c} (without arguments) to act as purely syntactic
   type: a nonterminal symbol of the inner syntax.
 
   \item @{command "syntax"}~@{text "(mode) decls"} is similar to
   @{command "consts"}~@{text decls}, except that the actual logical