equal
deleted
inserted
replaced
298 @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\ |
298 @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\ |
299 \end{matharray} |
299 \end{matharray} |
300 |
300 |
301 @{rail \<open> |
301 @{rail \<open> |
302 (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} | |
302 (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} | |
303 @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \<newline> |
303 @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline> |
304 ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} ) |
304 ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} ) |
305 ; |
305 ; |
|
306 @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} |
|
307 (@'for' (@{syntax vars} + @'and'))? |
|
308 ; |
306 @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) |
309 @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) |
|
310 (@'for' (@{syntax vars} + @'and'))? |
307 ; |
311 ; |
308 @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +) |
312 @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +) |
309 ; |
313 ; |
310 @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}? |
314 @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}? |
311 ; |
315 ; |
312 (@@{method tactic} | @@{method raw_tactic}) @{syntax text} |
316 (@@{method tactic} | @@{method raw_tactic}) @{syntax text} |
313 ; |
317 ; |
314 |
318 |
315 dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and') |
319 dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and') |
|
320 (@'for' (@{syntax vars} + @'and'))? |
316 \<close>} |
321 \<close>} |
317 |
322 |
318 \begin{description} |
323 \begin{description} |
319 |
324 |
320 \item @{method rule_tac} etc. do resolution of rules with explicit |
325 \item @{method rule_tac} etc. do resolution of rules with explicit |