doc-src/IsarRef/Thy/Document_Preparation.thy
changeset 40255 9ffbc25e1606
parent 39689 78b185bf7660
child 40800 330eb65c9469
     1.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Fri Oct 29 11:35:47 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Fri Oct 29 11:49:56 2010 +0200
     1.3 @@ -84,7 +84,7 @@
     1.4    \begin{rail}
     1.5      ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
     1.6      ;
     1.7 -    ('header' | 'text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
     1.8 +    ('header' | 'text_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt_raw') text
     1.9      ;
    1.10    \end{rail}
    1.11  
    1.12 @@ -198,10 +198,10 @@
    1.13        'goals' options |
    1.14        'subgoals' options |
    1.15        'prf' options thmrefs |
    1.16 -      'full\_prf' options thmrefs |
    1.17 +      'full_prf' options thmrefs |
    1.18        'ML' options name |
    1.19 -      'ML\_type' options name |
    1.20 -      'ML\_struct' options name
    1.21 +      'ML_type' options name |
    1.22 +      'ML_struct' options name
    1.23      ;
    1.24      options: '[' (option * ',') ']'
    1.25      ;
    1.26 @@ -468,7 +468,7 @@
    1.27    \end{matharray}
    1.28  
    1.29    \begin{rail}
    1.30 -    ('display\_drafts' | 'print\_drafts') (name +)
    1.31 +    ('display_drafts' | 'print_drafts') (name +)
    1.32      ;
    1.33    \end{rail}
    1.34