doc-src/IsarRef/Thy/Generic.thy

--- a/doc-src/IsarRef/Thy/Generic.thy	Fri Oct 29 11:35:47 2010 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Fri Oct 29 11:49:56 2010 +0200
@@ -284,14 +284,14 @@
   \end{matharray}
 
   \begin{rail}
-    ( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec?
+    ( 'rule_tac' | 'erule_tac' | 'drule_tac' | 'frule_tac' | 'cut_tac' | 'thin_tac' ) goalspec?
     ( insts thmref | thmrefs )
     ;
-    'subgoal\_tac' goalspec? (prop +)
+    'subgoal_tac' goalspec? (prop +)
     ;
-    'rename\_tac' goalspec? (name +)
+    'rename_tac' goalspec? (name +)
     ;
-    'rotate\_tac' goalspec? int?
+    'rotate_tac' goalspec? int?
     ;
     ('tactic' | 'raw_tactic') text
     ;
@@ -364,10 +364,10 @@
 
   \indexouternonterm{simpmod}
   \begin{rail}
-    ('simp' | 'simp\_all') opt? (simpmod *)
+    ('simp' | 'simp_all') opt? (simpmod *)
     ;
 
-    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
+    opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
     ;
     simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
       'split' (() | 'add' | 'del')) ':' thmrefs
@@ -471,7 +471,7 @@
   \end{matharray}
 
   \begin{rail}
-    'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
+    'simproc_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
     ;
 
     'simproc' (('add' ':')? | 'del' ':') (name+)
@@ -519,7 +519,7 @@
     'simplified' opt? thmrefs?
     ;
 
-    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use') ')'
+    opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
     ;
   \end{rail}
 
@@ -785,7 +785,7 @@
     ;
     'atomize' ('(' 'full' ')')?
     ;
-    'rule\_format' ('(' 'noasm' ')')?
+    'rule_format' ('(' 'noasm' ')')?
     ;
   \end{rail}