src/Doc/Isar_Ref/Inner_Syntax.thy
changeset 67513 731b1ad6759a
parent 67448 dbb1f02e667d
child 67718 17874d43d3b3
     1.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Jan 27 16:37:41 2018 +0100
     1.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Jan 27 16:45:27 2018 +0100
     1.3 @@ -850,12 +850,11 @@
     1.4      \<^descr> \<open>lexicon\<close> lists the delimiters of the inner token language; see
     1.5      \secref{sec:inner-lex}.
     1.6  
     1.7 -    \<^descr> \<open>prods\<close> lists the productions of the underlying priority grammar; see
     1.8 -    \secref{sec:priority-grammar}.
     1.9 +    \<^descr> \<open>productions\<close> lists the productions of the underlying priority grammar;
    1.10 +    see \secref{sec:priority-grammar}.
    1.11  
    1.12 -    The nonterminal \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> is rendered in plain text as \<open>A[p]\<close>; delimiters
    1.13 -    are quoted. Many productions have an extra \<open>\<dots> => name\<close>. These names later
    1.14 -    become the heads of parse trees; they also guide the pretty printer.
    1.15 +    Many productions have an extra \<open>\<dots> \<^bold>\<Rightarrow> name\<close>. These names later become the
    1.16 +    heads of parse trees; they also guide the pretty printer.
    1.17  
    1.18      Productions without such parse tree names are called \<^emph>\<open>copy productions\<close>.
    1.19      Their right-hand side must have exactly one nonterminal symbol (or named
    1.20 @@ -866,8 +865,7 @@
    1.21      nonterminal without any delimiters, then it is called a \<^emph>\<open>chain
    1.22      production\<close>. Chain productions act as abbreviations: conceptually, they
    1.23      are removed from the grammar by adding new productions. Priority
    1.24 -    information attached to chain productions is ignored; only the dummy value
    1.25 -    \<open>-1\<close> is displayed.
    1.26 +    information attached to chain productions is ignored.
    1.27  
    1.28      \<^descr> \<open>print modes\<close> lists the alternative print modes provided by this
    1.29      grammar; see \secref{sec:print-modes}.