--- a/doc-src/IsarRef/Thy/Generic.thy Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Thu May 05 23:23:02 2011 +0200
@@ -292,14 +292,14 @@
@{rail "
(@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
- @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goalspec}? \\
+ @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \\
( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
;
- @@{method subgoal_tac} @{syntax goalspec}? (@{syntax prop} +)
+ @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +)
;
- @@{method rename_tac} @{syntax goalspec}? (@{syntax name} +)
+ @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
;
- @@{method rotate_tac} @{syntax goalspec}? @{syntax int}?
+ @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
;
(@@{method tactic} | @@{method raw_tactic}) @{syntax text}
;