src/Doc/Isar_Ref/Proof_Script.thy

     @{command_def "prefer"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow> proof\<close> \\
     @{command_def "back"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow> proof\<close> \\
   \end{matharray}
 
   @{rail \<open>
-    @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
+    @@{command supply} (@{syntax thmdef}? @{syntax thms} + @'and')
     ;
     ( @@{command apply} | @@{command apply_end} ) @{syntax method}
     ;
     @@{command defer} @{syntax nat}?
     ;

   \end{matharray}
 
   @{rail \<open>
     (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
       @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
-    (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thmref} | @{syntax thmrefs} )
+    (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thm} | @{syntax thms} )
     ;
     @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
     ;
     @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}
     ;