doc-src/IsarRef/Thy/document/Inner_Syntax.tex
changeset 40255 9ffbc25e1606
parent 39279 878d86983dc1
child 40406 313a24b66a8d
     1.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Oct 29 11:35:47 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Oct 29 11:49:56 2010 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4      ;
     1.5      'thm' modes? thmrefs
     1.6      ;
     1.7 -    ( 'prf' | 'full\_prf' ) modes? thmrefs?
     1.8 +    ( 'prf' | 'full_prf' ) modes? thmrefs?
     1.9      ;
    1.10      'pr' modes? nat?
    1.11      ;
    1.12 @@ -387,9 +387,9 @@
    1.13    \end{matharray}
    1.14  
    1.15    \begin{rail}
    1.16 -    ('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and')
    1.17 +    ('type_notation' | 'no_type_notation') target? mode? \\ (nameref mixfix + 'and')
    1.18      ;
    1.19 -    ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
    1.20 +    ('notation' | 'no_notation') target? mode? \\ (nameref structmixfix + 'and')
    1.21      ;
    1.22      'write' mode? (nameref structmixfix + 'and')
    1.23      ;
    1.24 @@ -749,9 +749,9 @@
    1.25    \begin{rail}
    1.26      'nonterminals' (name +)
    1.27      ;
    1.28 -    ('syntax' | 'no\_syntax') mode? (constdecl +)
    1.29 +    ('syntax' | 'no_syntax') mode? (constdecl +)
    1.30      ;
    1.31 -    ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
    1.32 +    ('translations' | 'no_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
    1.33      ;
    1.34  
    1.35      mode: ('(' ( name | 'output' | name 'output' ) ')')
    1.36 @@ -806,8 +806,8 @@
    1.37    \end{matharray}
    1.38  
    1.39    \begin{rail}
    1.40 -  ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
    1.41 -    'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
    1.42 +  ( 'parse_ast_translation' | 'parse_translation' | 'print_translation' |
    1.43 +    'typed_print_translation' | 'print_ast_translation' ) ('(advanced)')? text
    1.44    ;
    1.45    \end{rail}
    1.46