doc-src/IsarRef/Thy/Inner_Syntax.thy

     ;
     'prop' modes? prop
     ;
     'thm' modes? thmrefs
     ;
-    ( 'prf' | 'full\_prf' ) modes? thmrefs?
+    ( 'prf' | 'full_prf' ) modes? thmrefs?
     ;
     'pr' modes? nat?
     ;
 
     modes: '(' (name + ) ')'

     @{command_def "no_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "write"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
   \end{matharray}
 
   \begin{rail}
-    ('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and')
-    ;
-    ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
+    ('type_notation' | 'no_type_notation') target? mode? \\ (nameref mixfix + 'and')
+    ;
+    ('notation' | 'no_notation') target? mode? \\ (nameref structmixfix + 'and')
     ;
     'write' mode? (nameref structmixfix + 'and')
     ;
   \end{rail}
 

   \end{matharray}
 
   \begin{rail}
     'nonterminals' (name +)
     ;
-    ('syntax' | 'no\_syntax') mode? (constdecl +)
-    ;
-    ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
+    ('syntax' | 'no_syntax') mode? (constdecl +)
+    ;
+    ('translations' | 'no_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
     ;
 
     mode: ('(' ( name | 'output' | name 'output' ) ')')
     ;
     transpat: ('(' nameref ')')? string

     @{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
   \end{matharray}
 
   \begin{rail}
-  ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
-    'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
+  ( 'parse_ast_translation' | 'parse_translation' | 'print_translation' |
+    'typed_print_translation' | 'print_ast_translation' ) ('(advanced)')? text
   ;
   \end{rail}
 
   Syntax translation functions written in ML admit almost arbitrary
   manipulations of Isabelle's inner syntax.  Any of the above commands