src/Doc/Isar_Ref/Generic.thy

--- a/src/Doc/Isar_Ref/Generic.thy	Mon Mar 23 10:16:20 2015 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy	Mon Mar 23 13:30:59 2015 +0100
@@ -300,10 +300,14 @@
 
   @{rail \<open>
     (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
-      @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \<newline>
+      @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
     ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
     ;
+    @@{method thin_tac} @{syntax goal_spec}? @{syntax prop}
+    (@'for' (@{syntax vars} + @'and'))?
+    ;
     @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +)
+    (@'for' (@{syntax vars} + @'and'))?
     ;
     @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
     ;
@@ -313,6 +317,7 @@
     ;
 
     dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and')
+    (@'for' (@{syntax vars} + @'and'))?
   \<close>}
 
 \begin{description}