345 |
345 |
346 \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a |
346 \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a |
347 goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the |
347 goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the |
348 \emph{suffix} of variables. |
348 \emph{suffix} of variables. |
349 |
349 |
350 \item @{method rotate_tac}~@{text n} rotates the assumptions of a |
350 \item @{method rotate_tac}~@{text n} rotates the premises of a |
351 goal by @{text n} positions: from right to left if @{text n} is |
351 subgoal by @{text n} positions: from right to left if @{text n} is |
352 positive, and from left to right if @{text n} is negative; the |
352 positive, and from left to right if @{text n} is negative; the |
353 default value is 1. See also @{ML rotate_tac} in |
353 default value is 1. |
354 \cite{isabelle-implementation}. |
|
355 |
354 |
356 \item @{method tactic}~@{text "text"} produces a proof method from |
355 \item @{method tactic}~@{text "text"} produces a proof method from |
357 any ML text of type @{ML_type tactic}. Apart from the usual ML |
356 any ML text of type @{ML_type tactic}. Apart from the usual ML |
358 environment and the current proof context, the ML code may refer to |
357 environment and the current proof context, the ML code may refer to |
359 the locally bound values @{ML_text facts}, which indicates any |
358 the locally bound values @{ML_text facts}, which indicates any |