summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 13 Mar 2000 16:24:23 +0100 | |

changeset 8443 | 0ed4b608ba4b |

parent 8442 | 96023903c2df |

child 8444 | 8f8eb220d9aa |

renamed cases_tac to case_tac;

--- a/doc-src/HOL/HOL.tex Mon Mar 13 16:23:34 2000 +0100 +++ b/doc-src/HOL/HOL.tex Mon Mar 13 16:24:23 2000 +0100 @@ -439,9 +439,9 @@ \item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI} repeatedly to remove all outermost universal quantifiers and implications from subgoal $i$. -\item[\ttindexbold{cases_tac} {\tt"}$P${\tt"} $i$] performs case distinction - on $P$ for subgoal $i$: the latter is replaced by two identical subgoals - with the added assumptions $P$ and $\lnot P$, respectively. +\item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction on + $P$ for subgoal $i$: the latter is replaced by two identical subgoals with + the added assumptions $P$ and $\lnot P$, respectively. \item[\ttindexbold{smp_tac} $j$ $i$] applies $j$ times \texttt{spec} and then \texttt{mp} in subgoal $i$, which is typically useful when forward-chaining from an induction hypothesis. As a generalization of \texttt{mp_tac}, @@ -2198,7 +2198,7 @@ In some cases, induction is overkill and a case distinction over all constructors of the datatype suffices. \begin{ttdescription} -\item[\ttindexbold{cases_tac} {\tt"}$u${\tt"} $i$] +\item[\ttindexbold{case_tac} {\tt"}$u${\tt"} $i$] performs a case analysis for the term $u$ whose type must be a datatype. If the datatype has $k@j$ constructors $C^j@1$, \dots $C^j@{k@j}$, subgoal $i$ is replaced by $k@j$ new subgoals which contain the additional @@ -2242,7 +2242,7 @@ For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt +}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section, but by more primitive means using \texttt{typedef}. To be able to use the -tactics \texttt{induct_tac} and \texttt{cases_tac} and to define functions by +tactics \texttt{induct_tac} and \texttt{case_tac} and to define functions by primitive recursion on these types, such types may be represented as actual datatypes. This is done by specifying an induction rule, as well as theorems stating the distinctness and injectivity of constructors in a {\tt