doc-src/IsarRef/Thy/document/Proof.tex

   contexts of (essentially a big disjunction of eliminated parameters
   and assumptions, cf.\ \secref{sec:obtain}).
 
   \begin{rail}
     ('lemma' | 'theorem' | 'corollary' |
-     'schematic\_lemma' | 'schematic\_theorem' | 'schematic\_corollary') target? (goal | longgoal)
+     'schematic_lemma' | 'schematic_theorem' | 'schematic_corollary') target? (goal | longgoal)
     ;
     ('have' | 'show' | 'hence' | 'thus') goal
     ;
-    'print\_statement' modes? thmrefs
+    'print_statement' modes? thmrefs
     ;
   
     goal: (props + 'and')
     ;
     longgoal: thmdecl? (contextelem *) conclusion

     \indexdef{}{command}{prefer}\hypertarget{command.prefer}{\hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
     \indexdef{}{command}{back}\hypertarget{command.back}{\hyperlink{command.back}{\mbox{\isa{\isacommand{back}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
   \end{matharray}
 
   \begin{rail}
-    ( 'apply' | 'apply\_end' ) method
+    ( 'apply' | 'apply_end' ) method
     ;
     'defer' nat?
     ;
     'prefer' nat
     ;

 \begin{matharray}{rcl}
     \indexdef{}{command}{method\_setup}\hypertarget{command.method-setup}{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   \end{matharray}
 
   \begin{rail}
-    'method\_setup' name '=' text text
+    'method_setup' name '=' text text
     ;
   \end{rail}
 
   \begin{description}
 

     'case' (caseref | '(' caseref ((name | underscore) +) ')')
     ;
     caseref: nameref attributes?
     ;
 
-    'case\_names' (name +)
-    ;
-    'case\_conclusion' name (name *)
+    'case_names' (name +)
+    ;
+    'case_conclusion' name (name *)
     ;
     'params' ((name *) + 'and')
     ;
     'consumes' nat?
     ;