doc-src/IsarRef/generic.tex
changeset 10627 dc3eff1b7556
parent 10548 e8c774c12105
child 10741 e56ac1863f2c
equal deleted inserted replaced
10626:46bcddfe9e7b 10627:dc3eff1b7556
   199   abbreviates $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
   199   abbreviates $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
   200 \item [$\isarkeyword{print_cases}$] prints all local contexts of the current
   200 \item [$\isarkeyword{print_cases}$] prints all local contexts of the current
   201   state, using Isar proof language notation.  This is a diagnostic command;
   201   state, using Isar proof language notation.  This is a diagnostic command;
   202   $undo$ does not apply.
   202   $undo$ does not apply.
   203 \item [$case_names~\vec c$] declares names for the local contexts of premises
   203 \item [$case_names~\vec c$] declares names for the local contexts of premises
   204   of some theorem; $\vec c$ refers to the \emph{suffix} of the list premises.
   204   of some theorem; $\vec c$ refers to the \emph{suffix} of the list of
       
   205   premises.
   205 \item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of
   206 \item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of
   206   premises $1, \dots, n$ of some theorem.  An empty list of names may be given
   207   premises $1, \dots, n$ of some theorem.  An empty list of names may be given
   207   to skip positions, leaving the present parameters unchanged.
   208   to skip positions, leaving the present parameters unchanged.
   208 
   209 
   209   Note that the default usage of case rules does \emph{not} directly expose
   210   Note that the default usage of case rules does \emph{not} directly expose