doc-src/IsarRef/Thy/document/Generic.tex
changeset 40255 9ffbc25e1606
parent 35613 9d3ff36ad4e1
child 40291 012ed4426fda
     1.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Fri Oct 29 11:35:47 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Fri Oct 29 11:49:56 2010 +0200
     1.3 @@ -302,14 +302,14 @@
     1.4    \end{matharray}
     1.5  
     1.6    \begin{rail}
     1.7 -    ( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec?
     1.8 +    ( 'rule_tac' | 'erule_tac' | 'drule_tac' | 'frule_tac' | 'cut_tac' | 'thin_tac' ) goalspec?
     1.9      ( insts thmref | thmrefs )
    1.10      ;
    1.11 -    'subgoal\_tac' goalspec? (prop +)
    1.12 +    'subgoal_tac' goalspec? (prop +)
    1.13      ;
    1.14 -    'rename\_tac' goalspec? (name +)
    1.15 +    'rename_tac' goalspec? (name +)
    1.16      ;
    1.17 -    'rotate\_tac' goalspec? int?
    1.18 +    'rotate_tac' goalspec? int?
    1.19      ;
    1.20      ('tactic' | 'raw_tactic') text
    1.21      ;
    1.22 @@ -384,10 +384,10 @@
    1.23  
    1.24    \indexouternonterm{simpmod}
    1.25    \begin{rail}
    1.26 -    ('simp' | 'simp\_all') opt? (simpmod *)
    1.27 +    ('simp' | 'simp_all') opt? (simpmod *)
    1.28      ;
    1.29  
    1.30 -    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
    1.31 +    opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
    1.32      ;
    1.33      simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
    1.34        'split' (() | 'add' | 'del')) ':' thmrefs
    1.35 @@ -490,7 +490,7 @@
    1.36    \end{matharray}
    1.37  
    1.38    \begin{rail}
    1.39 -    'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
    1.40 +    'simproc_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
    1.41      ;
    1.42  
    1.43      'simproc' (('add' ':')? | 'del' ':') (name+)
    1.44 @@ -538,7 +538,7 @@
    1.45      'simplified' opt? thmrefs?
    1.46      ;
    1.47  
    1.48 -    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use') ')'
    1.49 +    opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
    1.50      ;
    1.51    \end{rail}
    1.52  
    1.53 @@ -809,7 +809,7 @@
    1.54      ;
    1.55      'atomize' ('(' 'full' ')')?
    1.56      ;
    1.57 -    'rule\_format' ('(' 'noasm' ')')?
    1.58 +    'rule_format' ('(' 'noasm' ')')?
    1.59      ;
    1.60    \end{rail}
    1.61