1.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Fri Oct 29 11:35:47 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Fri Oct 29 11:49:56 2010 +0200
     1.3 @@ -453,11 +453,11 @@
     1.4  
     1.5    \begin{rail}
     1.6      ('lemma' | 'theorem' | 'corollary' |
     1.7 -     'schematic\_lemma' | 'schematic\_theorem' | 'schematic\_corollary') target? (goal | longgoal)
     1.8 +     'schematic_lemma' | 'schematic_theorem' | 'schematic_corollary') target? (goal | longgoal)
     1.9      ;
    1.10      ('have' | 'show' | 'hence' | 'thus') goal
    1.11      ;
    1.12 -    'print\_statement' modes? thmrefs
    1.13 +    'print_statement' modes? thmrefs
    1.14      ;
    1.15    
    1.16      goal: (props + 'and')
    1.17 @@ -843,7 +843,7 @@
    1.18    \end{matharray}
    1.19  
    1.20    \begin{rail}
    1.21 -    ( 'apply' | 'apply\_end' ) method
    1.22 +    ( 'apply' | 'apply_end' ) method
    1.23      ;
    1.24      'defer' nat?
    1.25      ;
    1.26 @@ -903,7 +903,7 @@
    1.27    \end{matharray}
    1.28  
    1.29    \begin{rail}
    1.30 -    'method\_setup' name '=' text text
    1.31 +    'method_setup' name '=' text text
    1.32      ;
    1.33    \end{rail}
    1.34  
    1.35 @@ -1192,9 +1192,9 @@
    1.36      caseref: nameref attributes?
    1.37      ;
    1.38  
    1.39 -    'case\_names' (name +)
    1.40 +    'case_names' (name +)
    1.41      ;
    1.42 -    'case\_conclusion' name (name *)
    1.43 +    'case_conclusion' name (name *)
    1.44      ;
    1.45      'params' ((name *) + 'and')
    1.46      ;