author wenzelm Mon, 23 Aug 1999 16:58:00 +0200 changeset 7328 4265615b4206 parent 7327 596318fdb379 child 7329 9053ad9a9768
record_simproc;
 doc-src/HOL/HOL.tex file | annotate | diff | comparison | revisions
--- 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

+\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

-\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}