doc-src/IsarRef/Thy/Inner_Syntax.thy
changeset 46512 4f9f61f9b535
parent 46506 c7faa011bfa7
child 48113 1c4500446ba4
     1.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Feb 17 11:24:39 2012 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Feb 17 15:42:26 2012 +0100
     1.3 @@ -980,7 +980,7 @@
     1.4  
     1.5  text {*
     1.6    \begin{tabular}{rcll}
     1.7 -    @{attribute_def syntax_ambiguity} & : & @{text attribute} & default @{text warning} \\
     1.8 +    @{attribute_def syntax_ambiguity_warning} & : & @{text attribute} & default @{text true} \\
     1.9      @{attribute_def syntax_ambiguity_limit} & : & @{text attribute} & default @{text 10} \\
    1.10    \end{tabular}
    1.11  
    1.12 @@ -1000,9 +1000,8 @@
    1.13  
    1.14    \begin{description}
    1.15  
    1.16 -  \item @{attribute syntax_ambiguity} determines reaction on multiple
    1.17 -  results of parsing; this string option can be set to @{text
    1.18 -  "ignore"}, @{text "warning"}, or @{text "error"}.
    1.19 +  \item @{attribute syntax_ambiguity_warning} controls output of
    1.20 +  explicit warning messages about syntax ambiguity.
    1.21  
    1.22    \item @{attribute syntax_ambiguity_limit} determines the number of
    1.23    resulting parse trees that are shown as part of the printed message