summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/HOL/HOL.tex

changeset 7328 | 4265615b4206 |

parent 7325 | 01bb8abb5a91 |

child 7490 | 9a74b57740d1 |

--- a/doc-src/HOL/HOL.tex Mon Aug 23 16:51:48 1999 +0200 +++ b/doc-src/HOL/HOL.tex Mon Aug 23 16:58:00 1999 +0200 @@ -1855,21 +1855,24 @@ terms, make function definitions) are part of the standard simpset (via \texttt{addsimps}). +\item Selectors applied to updated records are automatically reduced by + simplification procedure \ttindex{record_simproc}, which is part of the + default simpset. + \item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x' \conj y=y'$ are made part of the standard simpset and claset (via \texttt{addIffs}). -\item A tactic for record field splitting (\ttindex{record_split_tac}) is made - part of the standard claset (via \texttt{addSWrapper}). This tactic is - based on rules analogous to $(\All x PROP~P~x) \equiv (\All{a~b} PROP~P(a, - b))$ for any field. +\item A tactic for record field splitting (\ttindex{record_split_tac}) may be + made part of the claset (via \texttt{addSWrapper}). This tactic is based on + rules analogous to $(\All x PROP~P~x) \equiv (\All{a~b} PROP~P(a, b))$ for + any field. \end{enumerate} The first two kinds of rules are stored within the theory as $t\dtt simps$ and $t\dtt iffs$, respectively. In some situations it might be appropriate to -expand the definitions of updates: $t\dtt updates$. Following a new trend in -Isabelle system architecture, these names are \emph{not} bound at the {\ML} -level, though. +expand the definitions of updates: $t\dtt update_defs$. Note that these names +are \emph{not} bound at the {\ML} level. \medskip @@ -1878,7 +1881,8 @@ expand quantified record variables and then simplify by the conversion rules. By using a combination of the simplifier and classical prover together with the default simpset and claset, record problems should be solved with a single -stroke of \texttt{Auto_tac} or \texttt{Force_tac}. +stroke of \texttt{Auto_tac} or \texttt{Force_tac}. Most of the time, plain +\texttt{Simp_tac} should be sufficient, though. \section{Datatype definitions}