eliminated obsolete \_ escapes in rail environments;
authorwenzelm
Fri Oct 29 11:49:56 2010 +0200 (2010-10-29)
changeset 402559ffbc25e1606
parent 40254 6d1ebaa7a4ba
child 40256 eb5412b77ac4
eliminated obsolete \_ escapes in rail environments;
doc-src/IsarImplementation/Thy/Logic.thy
doc-src/IsarImplementation/Thy/document/Logic.tex
doc-src/IsarRef/Thy/Document_Preparation.thy
doc-src/IsarRef/Thy/Generic.thy
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/Inner_Syntax.thy
doc-src/IsarRef/Thy/Misc.thy
doc-src/IsarRef/Thy/Proof.thy
doc-src/IsarRef/Thy/Spec.thy
doc-src/IsarRef/Thy/ZF_Specific.thy
doc-src/IsarRef/Thy/document/Document_Preparation.tex
doc-src/IsarRef/Thy/document/Generic.tex
doc-src/IsarRef/Thy/document/HOL_Specific.tex
doc-src/IsarRef/Thy/document/Inner_Syntax.tex
doc-src/IsarRef/Thy/document/Misc.tex
doc-src/IsarRef/Thy/document/Proof.tex
doc-src/IsarRef/Thy/document/Spec.tex
doc-src/IsarRef/Thy/document/ZF_Specific.tex
     1.1 --- a/doc-src/IsarImplementation/Thy/Logic.thy	Fri Oct 29 11:35:47 2010 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/Logic.thy	Fri Oct 29 11:49:56 2010 +0200
     1.3 @@ -201,7 +201,7 @@
     1.4    ;
     1.5    'sort' sort
     1.6    ;
     1.7 -  ('type\_name' | 'type\_abbrev' | 'nonterminal') nameref
     1.8 +  ('type_name' | 'type_abbrev' | 'nonterminal') nameref
     1.9    ;
    1.10    'typ' type
    1.11    ;
    1.12 @@ -437,7 +437,7 @@
    1.13    \end{matharray}
    1.14  
    1.15    \begin{rail}
    1.16 -  ('const\_name' | 'const\_abbrev') nameref
    1.17 +  ('const_name' | 'const_abbrev') nameref
    1.18    ;
    1.19    'const' ('(' (type + ',') ')')?
    1.20    ;
     2.1 --- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Fri Oct 29 11:35:47 2010 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Fri Oct 29 11:49:56 2010 +0200
     2.3 @@ -218,7 +218,7 @@
     2.4    ;
     2.5    'sort' sort
     2.6    ;
     2.7 -  ('type\_name' | 'type\_abbrev' | 'nonterminal') nameref
     2.8 +  ('type_name' | 'type_abbrev' | 'nonterminal') nameref
     2.9    ;
    2.10    'typ' type
    2.11    ;
    2.12 @@ -464,7 +464,7 @@
    2.13    \end{matharray}
    2.14  
    2.15    \begin{rail}
    2.16 -  ('const\_name' | 'const\_abbrev') nameref
    2.17 +  ('const_name' | 'const_abbrev') nameref
    2.18    ;
    2.19    'const' ('(' (type + ',') ')')?
    2.20    ;
     3.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Fri Oct 29 11:35:47 2010 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Fri Oct 29 11:49:56 2010 +0200
     3.3 @@ -84,7 +84,7 @@
     3.4    \begin{rail}
     3.5      ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
     3.6      ;
     3.7 -    ('header' | 'text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
     3.8 +    ('header' | 'text_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt_raw') text
     3.9      ;
    3.10    \end{rail}
    3.11  
    3.12 @@ -198,10 +198,10 @@
    3.13        'goals' options |
    3.14        'subgoals' options |
    3.15        'prf' options thmrefs |
    3.16 -      'full\_prf' options thmrefs |
    3.17 +      'full_prf' options thmrefs |
    3.18        'ML' options name |
    3.19 -      'ML\_type' options name |
    3.20 -      'ML\_struct' options name
    3.21 +      'ML_type' options name |
    3.22 +      'ML_struct' options name
    3.23      ;
    3.24      options: '[' (option * ',') ']'
    3.25      ;
    3.26 @@ -468,7 +468,7 @@
    3.27    \end{matharray}
    3.28  
    3.29    \begin{rail}
    3.30 -    ('display\_drafts' | 'print\_drafts') (name +)
    3.31 +    ('display_drafts' | 'print_drafts') (name +)
    3.32      ;
    3.33    \end{rail}
    3.34  
     4.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Fri Oct 29 11:35:47 2010 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Fri Oct 29 11:49:56 2010 +0200
     4.3 @@ -284,14 +284,14 @@
     4.4    \end{matharray}
     4.5  
     4.6    \begin{rail}
     4.7 -    ( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec?
     4.8 +    ( 'rule_tac' | 'erule_tac' | 'drule_tac' | 'frule_tac' | 'cut_tac' | 'thin_tac' ) goalspec?
     4.9      ( insts thmref | thmrefs )
    4.10      ;
    4.11 -    'subgoal\_tac' goalspec? (prop +)
    4.12 +    'subgoal_tac' goalspec? (prop +)
    4.13      ;
    4.14 -    'rename\_tac' goalspec? (name +)
    4.15 +    'rename_tac' goalspec? (name +)
    4.16      ;
    4.17 -    'rotate\_tac' goalspec? int?
    4.18 +    'rotate_tac' goalspec? int?
    4.19      ;
    4.20      ('tactic' | 'raw_tactic') text
    4.21      ;
    4.22 @@ -364,10 +364,10 @@
    4.23  
    4.24    \indexouternonterm{simpmod}
    4.25    \begin{rail}
    4.26 -    ('simp' | 'simp\_all') opt? (simpmod *)
    4.27 +    ('simp' | 'simp_all') opt? (simpmod *)
    4.28      ;
    4.29  
    4.30 -    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
    4.31 +    opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
    4.32      ;
    4.33      simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
    4.34        'split' (() | 'add' | 'del')) ':' thmrefs
    4.35 @@ -471,7 +471,7 @@
    4.36    \end{matharray}
    4.37  
    4.38    \begin{rail}
    4.39 -    'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
    4.40 +    'simproc_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
    4.41      ;
    4.42  
    4.43      'simproc' (('add' ':')? | 'del' ':') (name+)
    4.44 @@ -519,7 +519,7 @@
    4.45      'simplified' opt? thmrefs?
    4.46      ;
    4.47  
    4.48 -    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use') ')'
    4.49 +    opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
    4.50      ;
    4.51    \end{rail}
    4.52  
    4.53 @@ -785,7 +785,7 @@
    4.54      ;
    4.55      'atomize' ('(' 'full' ')')?
    4.56      ;
    4.57 -    'rule\_format' ('(' 'noasm' ')')?
    4.58 +    'rule_format' ('(' 'noasm' ')')?
    4.59      ;
    4.60    \end{rail}
    4.61  
     5.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 29 11:35:47 2010 +0200
     5.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 29 11:49:56 2010 +0200
     5.3 @@ -72,7 +72,7 @@
     5.4    \end{matharray}
     5.5  
     5.6    \begin{rail}
     5.7 -    'split\_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
     5.8 +    'split_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
     5.9      ;
    5.10    \end{rail}
    5.11  
    5.12 @@ -355,7 +355,7 @@
    5.13    \begin{rail}
    5.14      'datatype' (dtspec + 'and')
    5.15      ;
    5.16 -    'rep\_datatype' ('(' (name +) ')')? (term +)
    5.17 +    'rep_datatype' ('(' (name +) ')')? (term +)
    5.18      ;
    5.19  
    5.20      dtspec: parname? typespec mixfix? '=' (cons + '|')
    5.21 @@ -501,9 +501,9 @@
    5.22    \begin{rail}
    5.23      'relation' term
    5.24      ;
    5.25 -    'lexicographic\_order' ( clasimpmod * )
    5.26 +    'lexicographic_order' ( clasimpmod * )
    5.27      ;
    5.28 -    'size\_change' ( orders ( clasimpmod * ) )
    5.29 +    'size_change' ( orders ( clasimpmod * ) )
    5.30      ;
    5.31      orders: ( 'max' | 'min' | 'ms' ) *
    5.32    \end{rail}
    5.33 @@ -633,7 +633,7 @@
    5.34      ;
    5.35      hints: '(' 'hints' ( recdefmod * ) ')'
    5.36      ;
    5.37 -    recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
    5.38 +    recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
    5.39      ;
    5.40      tc: nameref ('(' nat ')')?
    5.41      ;
    5.42 @@ -672,7 +672,7 @@
    5.43    \end{matharray}
    5.44  
    5.45    \begin{rail}
    5.46 -    ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del')
    5.47 +    ('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del')
    5.48      ;
    5.49    \end{rail}
    5.50  *}
    5.51 @@ -712,7 +712,7 @@
    5.52    \end{matharray}
    5.53  
    5.54    \begin{rail}
    5.55 -    ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\
    5.56 +    ('inductive' | 'inductive_set' | 'coinductive' | 'coinductive_set') target? fixes ('for' fixes)? \\
    5.57      ('where' clauses)? ('monos' thmrefs)?
    5.58      ;
    5.59      clauses: (thmdecl? prop + '|')
    5.60 @@ -991,13 +991,13 @@
    5.61    \end{matharray}
    5.62  
    5.63    \begin{rail}
    5.64 -    'case\_tac' goalspec? term rule?
    5.65 +    'case_tac' goalspec? term rule?
    5.66      ;
    5.67 -    'induct\_tac' goalspec? (insts * 'and') rule?
    5.68 +    'induct_tac' goalspec? (insts * 'and') rule?
    5.69      ;
    5.70 -    'ind\_cases' (prop +) ('for' (name +)) ?
    5.71 +    'ind_cases' (prop +) ('for' (name +)) ?
    5.72      ;
    5.73 -    'inductive\_cases' (thmdecl? (prop +) + 'and')
    5.74 +    'inductive_cases' (thmdecl? (prop +) + 'and')
    5.75      ;
    5.76  
    5.77      rule: ('rule' ':' thmref)
    5.78 @@ -1078,8 +1078,8 @@
    5.79    \end{matharray}
    5.80  
    5.81    \begin{rail}
    5.82 -     'export\_code' ( constexpr + ) \\
    5.83 -       ( ( 'in' target ( 'module\_name' string ) ? \\
    5.84 +     'export_code' ( constexpr + ) \\
    5.85 +       ( ( 'in' target ( 'module_name' string ) ? \\
    5.86          ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
    5.87      ;
    5.88  
    5.89 @@ -1101,10 +1101,10 @@
    5.90      'code' ( 'del' | 'abstype' | 'abstract' ) ?
    5.91      ;
    5.92  
    5.93 -    'code\_abort' ( const + )
    5.94 +    'code_abort' ( const + )
    5.95      ;
    5.96  
    5.97 -    'code\_datatype' ( const + )
    5.98 +    'code_datatype' ( const + )
    5.99      ;
   5.100  
   5.101      'code_inline' ( 'del' ) ?
   5.102 @@ -1113,41 +1113,41 @@
   5.103      'code_post' ( 'del' ) ?
   5.104      ;
   5.105  
   5.106 -    'code\_thms' ( constexpr + ) ?
   5.107 +    'code_thms' ( constexpr + ) ?
   5.108      ;
   5.109  
   5.110 -    'code\_deps' ( constexpr + ) ?
   5.111 +    'code_deps' ( constexpr + ) ?
   5.112      ;
   5.113  
   5.114 -    'code\_const' (const + 'and') \\
   5.115 +    'code_const' (const + 'and') \\
   5.116        ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
   5.117      ;
   5.118  
   5.119 -    'code\_type' (typeconstructor + 'and') \\
   5.120 +    'code_type' (typeconstructor + 'and') \\
   5.121        ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
   5.122      ;
   5.123  
   5.124 -    'code\_class' (class + 'and') \\
   5.125 +    'code_class' (class + 'and') \\
   5.126        ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
   5.127      ;
   5.128  
   5.129 -    'code\_instance' (( typeconstructor '::' class ) + 'and') \\
   5.130 +    'code_instance' (( typeconstructor '::' class ) + 'and') \\
   5.131        ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
   5.132      ;
   5.133  
   5.134 -    'code\_reserved' target ( string + )
   5.135 +    'code_reserved' target ( string + )
   5.136      ;
   5.137  
   5.138 -    'code\_monad' const const target
   5.139 +    'code_monad' const const target
   5.140      ;
   5.141  
   5.142 -    'code\_include' target ( string ( string | '-') )
   5.143 +    'code_include' target ( string ( string | '-') )
   5.144      ;
   5.145  
   5.146 -    'code\_modulename' target ( ( string string ) + )
   5.147 +    'code_modulename' target ( ( string string ) + )
   5.148      ;
   5.149  
   5.150 -    'code\_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
   5.151 +    'code_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
   5.152        ( 'functions' ( string + ) ) ? ( 'file' string ) ?
   5.153      ;
   5.154  
   5.155 @@ -1281,7 +1281,7 @@
   5.156    \end{matharray}
   5.157  
   5.158    \begin{rail}
   5.159 -  ( 'code\_module' | 'code\_library' ) modespec ? name ? \\
   5.160 +  ( 'code_module' | 'code_library' ) modespec ? name ? \\
   5.161      ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
   5.162      'contains' ( ( name '=' term ) + | term + )
   5.163    ;
   5.164 @@ -1289,13 +1289,13 @@
   5.165    modespec: '(' ( name * ) ')'
   5.166    ;
   5.167  
   5.168 -  'consts\_code' (codespec +)
   5.169 +  'consts_code' (codespec +)
   5.170    ;
   5.171  
   5.172    codespec: const template attachment ?
   5.173    ;
   5.174  
   5.175 -  'types\_code' (tycodespec +)
   5.176 +  'types_code' (tycodespec +)
   5.177    ;
   5.178  
   5.179    tycodespec: name template attachment ?
   5.180 @@ -1326,7 +1326,7 @@
   5.181    \end{matharray}
   5.182  
   5.183    \begin{rail}
   5.184 -  ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
   5.185 +  ('specification' | 'ax_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
   5.186    ;
   5.187    decl: ((name ':')? term '(' 'overloaded' ')'?)
   5.188    \end{rail}
     6.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Oct 29 11:35:47 2010 +0200
     6.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Oct 29 11:49:56 2010 +0200
     6.3 @@ -31,7 +31,7 @@
     6.4      ;
     6.5      'thm' modes? thmrefs
     6.6      ;
     6.7 -    ( 'prf' | 'full\_prf' ) modes? thmrefs?
     6.8 +    ( 'prf' | 'full_prf' ) modes? thmrefs?
     6.9      ;
    6.10      'pr' modes? nat?
    6.11      ;
    6.12 @@ -364,9 +364,9 @@
    6.13    \end{matharray}
    6.14  
    6.15    \begin{rail}
    6.16 -    ('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and')
    6.17 +    ('type_notation' | 'no_type_notation') target? mode? \\ (nameref mixfix + 'and')
    6.18      ;
    6.19 -    ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
    6.20 +    ('notation' | 'no_notation') target? mode? \\ (nameref structmixfix + 'and')
    6.21      ;
    6.22      'write' mode? (nameref structmixfix + 'and')
    6.23      ;
    6.24 @@ -730,9 +730,9 @@
    6.25    \begin{rail}
    6.26      'nonterminals' (name +)
    6.27      ;
    6.28 -    ('syntax' | 'no\_syntax') mode? (constdecl +)
    6.29 +    ('syntax' | 'no_syntax') mode? (constdecl +)
    6.30      ;
    6.31 -    ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
    6.32 +    ('translations' | 'no_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
    6.33      ;
    6.34  
    6.35      mode: ('(' ( name | 'output' | name 'output' ) ')')
    6.36 @@ -786,8 +786,8 @@
    6.37    \end{matharray}
    6.38  
    6.39    \begin{rail}
    6.40 -  ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
    6.41 -    'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
    6.42 +  ( 'parse_ast_translation' | 'parse_translation' | 'print_translation' |
    6.43 +    'typed_print_translation' | 'print_ast_translation' ) ('(advanced)')? text
    6.44    ;
    6.45    \end{rail}
    6.46  
     7.1 --- a/doc-src/IsarRef/Thy/Misc.thy	Fri Oct 29 11:35:47 2010 +0200
     7.2 +++ b/doc-src/IsarRef/Thy/Misc.thy	Fri Oct 29 11:49:56 2010 +0200
     7.3 @@ -21,19 +21,19 @@
     7.4    \end{matharray}
     7.5  
     7.6    \begin{rail}
     7.7 -    ('print\_theory' | 'print\_theorems') ('!'?)
     7.8 +    ('print_theory' | 'print_theorems') ('!'?)
     7.9      ;
    7.10  
    7.11 -    'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *)
    7.12 +    'find_theorems' (('(' (nat)? ('with_dups')? ')')?) (thmcriterion *)
    7.13      ;
    7.14      thmcriterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
    7.15        'solves' | 'simp' ':' term | term)
    7.16      ;
    7.17 -    'find\_consts' (constcriterion *)
    7.18 +    'find_consts' (constcriterion *)
    7.19      ;
    7.20      constcriterion: ('-'?) ('name' ':' nameref | 'strict' ':' type | type)
    7.21      ;
    7.22 -    'thm\_deps' thmrefs
    7.23 +    'thm_deps' thmrefs
    7.24      ;
    7.25    \end{rail}
    7.26  
    7.27 @@ -143,7 +143,7 @@
    7.28    \end{matharray}
    7.29  
    7.30    \begin{rail}
    7.31 -    ('cd' | 'use\_thy') name
    7.32 +    ('cd' | 'use_thy') name
    7.33      ;
    7.34    \end{rail}
    7.35  
     8.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Fri Oct 29 11:35:47 2010 +0200
     8.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Fri Oct 29 11:49:56 2010 +0200
     8.3 @@ -432,11 +432,11 @@
     8.4  
     8.5    \begin{rail}
     8.6      ('lemma' | 'theorem' | 'corollary' |
     8.7 -     'schematic\_lemma' | 'schematic\_theorem' | 'schematic\_corollary') target? (goal | longgoal)
     8.8 +     'schematic_lemma' | 'schematic_theorem' | 'schematic_corollary') target? (goal | longgoal)
     8.9      ;
    8.10      ('have' | 'show' | 'hence' | 'thus') goal
    8.11      ;
    8.12 -    'print\_statement' modes? thmrefs
    8.13 +    'print_statement' modes? thmrefs
    8.14      ;
    8.15    
    8.16      goal: (props + 'and')
    8.17 @@ -834,7 +834,7 @@
    8.18    \end{matharray}
    8.19  
    8.20    \begin{rail}
    8.21 -    ( 'apply' | 'apply\_end' ) method
    8.22 +    ( 'apply' | 'apply_end' ) method
    8.23      ;
    8.24      'defer' nat?
    8.25      ;
    8.26 @@ -896,7 +896,7 @@
    8.27    \end{matharray}
    8.28  
    8.29    \begin{rail}
    8.30 -    'method\_setup' name '=' text text
    8.31 +    'method_setup' name '=' text text
    8.32      ;
    8.33    \end{rail}
    8.34  
    8.35 @@ -1190,9 +1190,9 @@
    8.36      caseref: nameref attributes?
    8.37      ;
    8.38  
    8.39 -    'case\_names' (name +)
    8.40 +    'case_names' (name +)
    8.41      ;
    8.42 -    'case\_conclusion' name (name *)
    8.43 +    'case_conclusion' name (name *)
    8.44      ;
    8.45      'params' ((name *) + 'and')
    8.46      ;
     9.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Fri Oct 29 11:35:47 2010 +0200
     9.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Fri Oct 29 11:49:56 2010 +0200
     9.3 @@ -360,7 +360,7 @@
     9.4    \begin{rail}
     9.5      'locale' name ('=' locale)? 'begin'?
     9.6      ;
     9.7 -    'print\_locale' '!'? nameref
     9.8 +    'print_locale' '!'? nameref
     9.9      ;
    9.10      locale: contextelem+ | localeexpr ('+' (contextelem+))?
    9.11      ;
    9.12 @@ -503,7 +503,7 @@
    9.13      ;
    9.14      'interpret' localeexpr equations?
    9.15      ;
    9.16 -    'print\_interps' nameref
    9.17 +    'print_interps' nameref
    9.18      ;
    9.19      equations: 'where' (thmdecl? prop + 'and')
    9.20      ;
    9.21 @@ -630,9 +630,9 @@
    9.22      ;
    9.23      'instance' nameref ('<' | subseteq) nameref
    9.24      ;
    9.25 -    'print\_classes'
    9.26 +    'print_classes'
    9.27      ;
    9.28 -    'class\_deps'
    9.29 +    'class_deps'
    9.30      ;
    9.31  
    9.32      superclassexpr: nameref | (nameref '+' superclassexpr)
    9.33 @@ -840,9 +840,9 @@
    9.34    \begin{rail}
    9.35      'use' name
    9.36      ;
    9.37 -    ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
    9.38 +    ('ML' | 'ML_prf' | 'ML_val' | 'ML_command' | 'setup' | 'local_setup') text
    9.39      ;
    9.40 -    'attribute\_setup' name '=' text text
    9.41 +    'attribute_setup' name '=' text text
    9.42      ;
    9.43    \end{rail}
    9.44  
    9.45 @@ -930,7 +930,7 @@
    9.46      ;
    9.47      'classrel' (nameref ('<' | subseteq) nameref + 'and')
    9.48      ;
    9.49 -    'default\_sort' sort
    9.50 +    'default_sort' sort
    9.51      ;
    9.52    \end{rail}
    9.53  
    9.54 @@ -1176,7 +1176,7 @@
    9.55    \end{matharray}
    9.56  
    9.57    \begin{rail}
    9.58 -    ( 'hide\_class' | 'hide\_type' | 'hide\_const' | 'hide\_fact' ) ('(open)')? (nameref + )
    9.59 +    ( 'hide_class' | 'hide_type' | 'hide_const' | 'hide_fact' ) ('(open)')? (nameref + )
    9.60      ;
    9.61    \end{rail}
    9.62  
    10.1 --- a/doc-src/IsarRef/Thy/ZF_Specific.thy	Fri Oct 29 11:35:47 2010 +0200
    10.2 +++ b/doc-src/IsarRef/Thy/ZF_Specific.thy	Fri Oct 29 11:49:56 2010 +0200
    10.3 @@ -67,11 +67,11 @@
    10.4      ;
    10.5      monos: ('monos' thmrefs)?
    10.6      ;
    10.7 -    condefs: ('con\_defs' thmrefs)?
    10.8 +    condefs: ('con_defs' thmrefs)?
    10.9      ;
   10.10 -    typeintros: ('type\_intros' thmrefs)?
   10.11 +    typeintros: ('type_intros' thmrefs)?
   10.12      ;
   10.13 -    typeelims: ('type\_elims' thmrefs)?
   10.14 +    typeelims: ('type_elims' thmrefs)?
   10.15      ;
   10.16    \end{rail}
   10.17  
   10.18 @@ -126,7 +126,7 @@
   10.19    \end{matharray}
   10.20  
   10.21    \begin{rail}
   10.22 -    ('case\_tac' | 'induct\_tac') goalspec? name
   10.23 +    ('case_tac' | 'induct_tac') goalspec? name
   10.24      ;
   10.25      indcases (prop +)
   10.26      ;
    11.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Oct 29 11:35:47 2010 +0200
    11.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Oct 29 11:49:56 2010 +0200
    11.3 @@ -105,7 +105,7 @@
    11.4    \begin{rail}
    11.5      ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
    11.6      ;
    11.7 -    ('header' | 'text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
    11.8 +    ('header' | 'text_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt_raw') text
    11.9      ;
   11.10    \end{rail}
   11.11  
   11.12 @@ -216,10 +216,10 @@
   11.13        'goals' options |
   11.14        'subgoals' options |
   11.15        'prf' options thmrefs |
   11.16 -      'full\_prf' options thmrefs |
   11.17 +      'full_prf' options thmrefs |
   11.18        'ML' options name |
   11.19 -      'ML\_type' options name |
   11.20 -      'ML\_struct' options name
   11.21 +      'ML_type' options name |
   11.22 +      'ML_struct' options name
   11.23      ;
   11.24      options: '[' (option * ',') ']'
   11.25      ;
   11.26 @@ -487,7 +487,7 @@
   11.27    \end{matharray}
   11.28  
   11.29    \begin{rail}
   11.30 -    ('display\_drafts' | 'print\_drafts') (name +)
   11.31 +    ('display_drafts' | 'print_drafts') (name +)
   11.32      ;
   11.33    \end{rail}
   11.34  
    12.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Fri Oct 29 11:35:47 2010 +0200
    12.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Fri Oct 29 11:49:56 2010 +0200
    12.3 @@ -302,14 +302,14 @@
    12.4    \end{matharray}
    12.5  
    12.6    \begin{rail}
    12.7 -    ( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec?
    12.8 +    ( 'rule_tac' | 'erule_tac' | 'drule_tac' | 'frule_tac' | 'cut_tac' | 'thin_tac' ) goalspec?
    12.9      ( insts thmref | thmrefs )
   12.10      ;
   12.11 -    'subgoal\_tac' goalspec? (prop +)
   12.12 +    'subgoal_tac' goalspec? (prop +)
   12.13      ;
   12.14 -    'rename\_tac' goalspec? (name +)
   12.15 +    'rename_tac' goalspec? (name +)
   12.16      ;
   12.17 -    'rotate\_tac' goalspec? int?
   12.18 +    'rotate_tac' goalspec? int?
   12.19      ;
   12.20      ('tactic' | 'raw_tactic') text
   12.21      ;
   12.22 @@ -384,10 +384,10 @@
   12.23  
   12.24    \indexouternonterm{simpmod}
   12.25    \begin{rail}
   12.26 -    ('simp' | 'simp\_all') opt? (simpmod *)
   12.27 +    ('simp' | 'simp_all') opt? (simpmod *)
   12.28      ;
   12.29  
   12.30 -    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
   12.31 +    opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
   12.32      ;
   12.33      simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
   12.34        'split' (() | 'add' | 'del')) ':' thmrefs
   12.35 @@ -490,7 +490,7 @@
   12.36    \end{matharray}
   12.37  
   12.38    \begin{rail}
   12.39 -    'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
   12.40 +    'simproc_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
   12.41      ;
   12.42  
   12.43      'simproc' (('add' ':')? | 'del' ':') (name+)
   12.44 @@ -538,7 +538,7 @@
   12.45      'simplified' opt? thmrefs?
   12.46      ;
   12.47  
   12.48 -    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use') ')'
   12.49 +    opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
   12.50      ;
   12.51    \end{rail}
   12.52  
   12.53 @@ -809,7 +809,7 @@
   12.54      ;
   12.55      'atomize' ('(' 'full' ')')?
   12.56      ;
   12.57 -    'rule\_format' ('(' 'noasm' ')')?
   12.58 +    'rule_format' ('(' 'noasm' ')')?
   12.59      ;
   12.60    \end{rail}
   12.61  
    13.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 29 11:35:47 2010 +0200
    13.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 29 11:49:56 2010 +0200
    13.3 @@ -93,7 +93,7 @@
    13.4    \end{matharray}
    13.5  
    13.6    \begin{rail}
    13.7 -    'split\_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
    13.8 +    'split_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
    13.9      ;
   13.10    \end{rail}
   13.11  
   13.12 @@ -364,7 +364,7 @@
   13.13    \begin{rail}
   13.14      'datatype' (dtspec + 'and')
   13.15      ;
   13.16 -    'rep\_datatype' ('(' (name +) ')')? (term +)
   13.17 +    'rep_datatype' ('(' (name +) ')')? (term +)
   13.18      ;
   13.19  
   13.20      dtspec: parname? typespec mixfix? '=' (cons + '|')
   13.21 @@ -511,9 +511,9 @@
   13.22    \begin{rail}
   13.23      'relation' term
   13.24      ;
   13.25 -    'lexicographic\_order' ( clasimpmod * )
   13.26 +    'lexicographic_order' ( clasimpmod * )
   13.27      ;
   13.28 -    'size\_change' ( orders ( clasimpmod * ) )
   13.29 +    'size_change' ( orders ( clasimpmod * ) )
   13.30      ;
   13.31      orders: ( 'max' | 'min' | 'ms' ) *
   13.32    \end{rail}
   13.33 @@ -642,7 +642,7 @@
   13.34      ;
   13.35      hints: '(' 'hints' ( recdefmod * ) ')'
   13.36      ;
   13.37 -    recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
   13.38 +    recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
   13.39      ;
   13.40      tc: nameref ('(' nat ')')?
   13.41      ;
   13.42 @@ -680,7 +680,7 @@
   13.43    \end{matharray}
   13.44  
   13.45    \begin{rail}
   13.46 -    ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del')
   13.47 +    ('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del')
   13.48      ;
   13.49    \end{rail}%
   13.50  \end{isamarkuptext}%
   13.51 @@ -722,7 +722,7 @@
   13.52    \end{matharray}
   13.53  
   13.54    \begin{rail}
   13.55 -    ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\
   13.56 +    ('inductive' | 'inductive_set' | 'coinductive' | 'coinductive_set') target? fixes ('for' fixes)? \\
   13.57      ('where' clauses)? ('monos' thmrefs)?
   13.58      ;
   13.59      clauses: (thmdecl? prop + '|')
   13.60 @@ -1010,13 +1010,13 @@
   13.61    \end{matharray}
   13.62  
   13.63    \begin{rail}
   13.64 -    'case\_tac' goalspec? term rule?
   13.65 +    'case_tac' goalspec? term rule?
   13.66      ;
   13.67 -    'induct\_tac' goalspec? (insts * 'and') rule?
   13.68 +    'induct_tac' goalspec? (insts * 'and') rule?
   13.69      ;
   13.70 -    'ind\_cases' (prop +) ('for' (name +)) ?
   13.71 +    'ind_cases' (prop +) ('for' (name +)) ?
   13.72      ;
   13.73 -    'inductive\_cases' (thmdecl? (prop +) + 'and')
   13.74 +    'inductive_cases' (thmdecl? (prop +) + 'and')
   13.75      ;
   13.76  
   13.77      rule: ('rule' ':' thmref)
   13.78 @@ -1093,8 +1093,8 @@
   13.79    \end{matharray}
   13.80  
   13.81    \begin{rail}
   13.82 -     'export\_code' ( constexpr + ) \\
   13.83 -       ( ( 'in' target ( 'module\_name' string ) ? \\
   13.84 +     'export_code' ( constexpr + ) \\
   13.85 +       ( ( 'in' target ( 'module_name' string ) ? \\
   13.86          ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
   13.87      ;
   13.88  
   13.89 @@ -1116,10 +1116,10 @@
   13.90      'code' ( 'del' | 'abstype' | 'abstract' ) ?
   13.91      ;
   13.92  
   13.93 -    'code\_abort' ( const + )
   13.94 +    'code_abort' ( const + )
   13.95      ;
   13.96  
   13.97 -    'code\_datatype' ( const + )
   13.98 +    'code_datatype' ( const + )
   13.99      ;
  13.100  
  13.101      'code_inline' ( 'del' ) ?
  13.102 @@ -1128,41 +1128,41 @@
  13.103      'code_post' ( 'del' ) ?
  13.104      ;
  13.105  
  13.106 -    'code\_thms' ( constexpr + ) ?
  13.107 +    'code_thms' ( constexpr + ) ?
  13.108      ;
  13.109  
  13.110 -    'code\_deps' ( constexpr + ) ?
  13.111 +    'code_deps' ( constexpr + ) ?
  13.112      ;
  13.113  
  13.114 -    'code\_const' (const + 'and') \\
  13.115 +    'code_const' (const + 'and') \\
  13.116        ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
  13.117      ;
  13.118  
  13.119 -    'code\_type' (typeconstructor + 'and') \\
  13.120 +    'code_type' (typeconstructor + 'and') \\
  13.121        ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
  13.122      ;
  13.123  
  13.124 -    'code\_class' (class + 'and') \\
  13.125 +    'code_class' (class + 'and') \\
  13.126        ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
  13.127      ;
  13.128  
  13.129 -    'code\_instance' (( typeconstructor '::' class ) + 'and') \\
  13.130 +    'code_instance' (( typeconstructor '::' class ) + 'and') \\
  13.131        ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
  13.132      ;
  13.133  
  13.134 -    'code\_reserved' target ( string + )
  13.135 +    'code_reserved' target ( string + )
  13.136      ;
  13.137  
  13.138 -    'code\_monad' const const target
  13.139 +    'code_monad' const const target
  13.140      ;
  13.141  
  13.142 -    'code\_include' target ( string ( string | '-') )
  13.143 +    'code_include' target ( string ( string | '-') )
  13.144      ;
  13.145  
  13.146 -    'code\_modulename' target ( ( string string ) + )
  13.147 +    'code_modulename' target ( ( string string ) + )
  13.148      ;
  13.149  
  13.150 -    'code\_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
  13.151 +    'code_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
  13.152        ( 'functions' ( string + ) ) ? ( 'file' string ) ?
  13.153      ;
  13.154  
  13.155 @@ -1293,7 +1293,7 @@
  13.156    \end{matharray}
  13.157  
  13.158    \begin{rail}
  13.159 -  ( 'code\_module' | 'code\_library' ) modespec ? name ? \\
  13.160 +  ( 'code_module' | 'code_library' ) modespec ? name ? \\
  13.161      ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
  13.162      'contains' ( ( name '=' term ) + | term + )
  13.163    ;
  13.164 @@ -1301,13 +1301,13 @@
  13.165    modespec: '(' ( name * ) ')'
  13.166    ;
  13.167  
  13.168 -  'consts\_code' (codespec +)
  13.169 +  'consts_code' (codespec +)
  13.170    ;
  13.171  
  13.172    codespec: const template attachment ?
  13.173    ;
  13.174  
  13.175 -  'types\_code' (tycodespec +)
  13.176 +  'types_code' (tycodespec +)
  13.177    ;
  13.178  
  13.179    tycodespec: name template attachment ?
  13.180 @@ -1339,7 +1339,7 @@
  13.181    \end{matharray}
  13.182  
  13.183    \begin{rail}
  13.184 -  ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
  13.185 +  ('specification' | 'ax_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
  13.186    ;
  13.187    decl: ((name ':')? term '(' 'overloaded' ')'?)
  13.188    \end{rail}
    14.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Oct 29 11:35:47 2010 +0200
    14.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Oct 29 11:49:56 2010 +0200
    14.3 @@ -53,7 +53,7 @@
    14.4      ;
    14.5      'thm' modes? thmrefs
    14.6      ;
    14.7 -    ( 'prf' | 'full\_prf' ) modes? thmrefs?
    14.8 +    ( 'prf' | 'full_prf' ) modes? thmrefs?
    14.9      ;
   14.10      'pr' modes? nat?
   14.11      ;
   14.12 @@ -387,9 +387,9 @@
   14.13    \end{matharray}
   14.14  
   14.15    \begin{rail}
   14.16 -    ('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and')
   14.17 +    ('type_notation' | 'no_type_notation') target? mode? \\ (nameref mixfix + 'and')
   14.18      ;
   14.19 -    ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
   14.20 +    ('notation' | 'no_notation') target? mode? \\ (nameref structmixfix + 'and')
   14.21      ;
   14.22      'write' mode? (nameref structmixfix + 'and')
   14.23      ;
   14.24 @@ -749,9 +749,9 @@
   14.25    \begin{rail}
   14.26      'nonterminals' (name +)
   14.27      ;
   14.28 -    ('syntax' | 'no\_syntax') mode? (constdecl +)
   14.29 +    ('syntax' | 'no_syntax') mode? (constdecl +)
   14.30      ;
   14.31 -    ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
   14.32 +    ('translations' | 'no_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
   14.33      ;
   14.34  
   14.35      mode: ('(' ( name | 'output' | name 'output' ) ')')
   14.36 @@ -806,8 +806,8 @@
   14.37    \end{matharray}
   14.38  
   14.39    \begin{rail}
   14.40 -  ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
   14.41 -    'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
   14.42 +  ( 'parse_ast_translation' | 'parse_translation' | 'print_translation' |
   14.43 +    'typed_print_translation' | 'print_ast_translation' ) ('(advanced)')? text
   14.44    ;
   14.45    \end{rail}
   14.46  
    15.1 --- a/doc-src/IsarRef/Thy/document/Misc.tex	Fri Oct 29 11:35:47 2010 +0200
    15.2 +++ b/doc-src/IsarRef/Thy/document/Misc.tex	Fri Oct 29 11:49:56 2010 +0200
    15.3 @@ -41,19 +41,19 @@
    15.4    \end{matharray}
    15.5  
    15.6    \begin{rail}
    15.7 -    ('print\_theory' | 'print\_theorems') ('!'?)
    15.8 +    ('print_theory' | 'print_theorems') ('!'?)
    15.9      ;
   15.10  
   15.11 -    'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *)
   15.12 +    'find_theorems' (('(' (nat)? ('with_dups')? ')')?) (thmcriterion *)
   15.13      ;
   15.14      thmcriterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
   15.15        'solves' | 'simp' ':' term | term)
   15.16      ;
   15.17 -    'find\_consts' (constcriterion *)
   15.18 +    'find_consts' (constcriterion *)
   15.19      ;
   15.20      constcriterion: ('-'?) ('name' ':' nameref | 'strict' ':' type | type)
   15.21      ;
   15.22 -    'thm\_deps' thmrefs
   15.23 +    'thm_deps' thmrefs
   15.24      ;
   15.25    \end{rail}
   15.26  
   15.27 @@ -164,7 +164,7 @@
   15.28    \end{matharray}
   15.29  
   15.30    \begin{rail}
   15.31 -    ('cd' | 'use\_thy') name
   15.32 +    ('cd' | 'use_thy') name
   15.33      ;
   15.34    \end{rail}
   15.35  
    16.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Fri Oct 29 11:35:47 2010 +0200
    16.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Fri Oct 29 11:49:56 2010 +0200
    16.3 @@ -453,11 +453,11 @@
    16.4  
    16.5    \begin{rail}
    16.6      ('lemma' | 'theorem' | 'corollary' |
    16.7 -     'schematic\_lemma' | 'schematic\_theorem' | 'schematic\_corollary') target? (goal | longgoal)
    16.8 +     'schematic_lemma' | 'schematic_theorem' | 'schematic_corollary') target? (goal | longgoal)
    16.9      ;
   16.10      ('have' | 'show' | 'hence' | 'thus') goal
   16.11      ;
   16.12 -    'print\_statement' modes? thmrefs
   16.13 +    'print_statement' modes? thmrefs
   16.14      ;
   16.15    
   16.16      goal: (props + 'and')
   16.17 @@ -843,7 +843,7 @@
   16.18    \end{matharray}
   16.19  
   16.20    \begin{rail}
   16.21 -    ( 'apply' | 'apply\_end' ) method
   16.22 +    ( 'apply' | 'apply_end' ) method
   16.23      ;
   16.24      'defer' nat?
   16.25      ;
   16.26 @@ -903,7 +903,7 @@
   16.27    \end{matharray}
   16.28  
   16.29    \begin{rail}
   16.30 -    'method\_setup' name '=' text text
   16.31 +    'method_setup' name '=' text text
   16.32      ;
   16.33    \end{rail}
   16.34  
   16.35 @@ -1192,9 +1192,9 @@
   16.36      caseref: nameref attributes?
   16.37      ;
   16.38  
   16.39 -    'case\_names' (name +)
   16.40 +    'case_names' (name +)
   16.41      ;
   16.42 -    'case\_conclusion' name (name *)
   16.43 +    'case_conclusion' name (name *)
   16.44      ;
   16.45      'params' ((name *) + 'and')
   16.46      ;
    17.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Fri Oct 29 11:35:47 2010 +0200
    17.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Fri Oct 29 11:49:56 2010 +0200
    17.3 @@ -385,7 +385,7 @@
    17.4    \begin{rail}
    17.5      'locale' name ('=' locale)? 'begin'?
    17.6      ;
    17.7 -    'print\_locale' '!'? nameref
    17.8 +    'print_locale' '!'? nameref
    17.9      ;
   17.10      locale: contextelem+ | localeexpr ('+' (contextelem+))?
   17.11      ;
   17.12 @@ -525,7 +525,7 @@
   17.13      ;
   17.14      'interpret' localeexpr equations?
   17.15      ;
   17.16 -    'print\_interps' nameref
   17.17 +    'print_interps' nameref
   17.18      ;
   17.19      equations: 'where' (thmdecl? prop + 'and')
   17.20      ;
   17.21 @@ -653,9 +653,9 @@
   17.22      ;
   17.23      'instance' nameref ('<' | subseteq) nameref
   17.24      ;
   17.25 -    'print\_classes'
   17.26 +    'print_classes'
   17.27      ;
   17.28 -    'class\_deps'
   17.29 +    'class_deps'
   17.30      ;
   17.31  
   17.32      superclassexpr: nameref | (nameref '+' superclassexpr)
   17.33 @@ -862,9 +862,9 @@
   17.34    \begin{rail}
   17.35      'use' name
   17.36      ;
   17.37 -    ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
   17.38 +    ('ML' | 'ML_prf' | 'ML_val' | 'ML_command' | 'setup' | 'local_setup') text
   17.39      ;
   17.40 -    'attribute\_setup' name '=' text text
   17.41 +    'attribute_setup' name '=' text text
   17.42      ;
   17.43    \end{rail}
   17.44  
   17.45 @@ -966,7 +966,7 @@
   17.46      ;
   17.47      'classrel' (nameref ('<' | subseteq) nameref + 'and')
   17.48      ;
   17.49 -    'default\_sort' sort
   17.50 +    'default_sort' sort
   17.51      ;
   17.52    \end{rail}
   17.53  
   17.54 @@ -1218,7 +1218,7 @@
   17.55    \end{matharray}
   17.56  
   17.57    \begin{rail}
   17.58 -    ( 'hide\_class' | 'hide\_type' | 'hide\_const' | 'hide\_fact' ) ('(open)')? (nameref + )
   17.59 +    ( 'hide_class' | 'hide_type' | 'hide_const' | 'hide_fact' ) ('(open)')? (nameref + )
   17.60      ;
   17.61    \end{rail}
   17.62  
    18.1 --- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Fri Oct 29 11:35:47 2010 +0200
    18.2 +++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Fri Oct 29 11:49:56 2010 +0200
    18.3 @@ -91,11 +91,11 @@
    18.4      ;
    18.5      monos: ('monos' thmrefs)?
    18.6      ;
    18.7 -    condefs: ('con\_defs' thmrefs)?
    18.8 +    condefs: ('con_defs' thmrefs)?
    18.9      ;
   18.10 -    typeintros: ('type\_intros' thmrefs)?
   18.11 +    typeintros: ('type_intros' thmrefs)?
   18.12      ;
   18.13 -    typeelims: ('type\_elims' thmrefs)?
   18.14 +    typeelims: ('type_elims' thmrefs)?
   18.15      ;
   18.16    \end{rail}
   18.17  
   18.18 @@ -153,7 +153,7 @@
   18.19    \end{matharray}
   18.20  
   18.21    \begin{rail}
   18.22 -    ('case\_tac' | 'induct\_tac') goalspec? name
   18.23 +    ('case_tac' | 'induct_tac') goalspec? name
   18.24      ;
   18.25      indcases (prop +)
   18.26      ;