1853 
1853 
1854 \item Standard conversions (selectors or updates applied to record constructor 
1854 \item Standard conversions (selectors or updates applied to record constructor 
1855 terms, make function definitions) are part of the standard simpset (via 
1855 terms, make function definitions) are part of the standard simpset (via 
1856 \texttt{addsimps}). 
1856 \texttt{addsimps}). 
1857 
1857 

1858 \item Selectors applied to updated records are automatically reduced by 

1859 simplification procedure \ttindex{record_simproc}, which is part of the 

1860 default simpset. 

1861 
1858 \item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x' 
1862 \item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x' 
1859 \conj y=y'$ are made part of the standard simpset and claset (via 
1863 \conj y=y'$ are made part of the standard simpset and claset (via 
1860 \texttt{addIffs}). 
1864 \texttt{addIffs}). 
1861 
1865 
1862 \item A tactic for record field splitting (\ttindex{record_split_tac}) is made 
1866 \item A tactic for record field splitting (\ttindex{record_split_tac}) may be 
1863 part of the standard claset (via \texttt{addSWrapper}). This tactic is 
1867 made part of the claset (via \texttt{addSWrapper}). This tactic is based on 
1864 based on rules analogous to $(\All x PROP~P~x) \equiv (\All{a~b} PROP~P(a, 
1868 rules analogous to $(\All x PROP~P~x) \equiv (\All{a~b} PROP~P(a, b))$ for 
1865 b))$ for any field. 
1869 any field. 
1866 \end{enumerate} 
1870 \end{enumerate} 
1867 
1871 
1868 The first two kinds of rules are stored within the theory as $t\dtt simps$ and 
1872 The first two kinds of rules are stored within the theory as $t\dtt simps$ and 
1869 $t\dtt iffs$, respectively. In some situations it might be appropriate to 
1873 $t\dtt iffs$, respectively. In some situations it might be appropriate to 
1870 expand the definitions of updates: $t\dtt updates$. Following a new trend in 
1874 expand the definitions of updates: $t\dtt update_defs$. Note that these names 
1871 Isabelle system architecture, these names are \emph{not} bound at the {\ML} 
1875 are \emph{not} bound at the {\ML} level. 
1872 level, though. 

1873 
1876 
1874 \medskip 
1877 \medskip 
1875 
1878 
1876 The example theory \texttt{HOL/ex/Points} demonstrates typical proofs 
1879 The example theory \texttt{HOL/ex/Points} demonstrates typical proofs 
1877 concerning records. The basic idea is to make \ttindex{record_split_tac} 
1880 concerning records. The basic idea is to make \ttindex{record_split_tac} 
1878 expand quantified record variables and then simplify by the conversion rules. 
1881 expand quantified record variables and then simplify by the conversion rules. 
1879 By using a combination of the simplifier and classical prover together with 
1882 By using a combination of the simplifier and classical prover together with 
1880 the default simpset and claset, record problems should be solved with a single 
1883 the default simpset and claset, record problems should be solved with a single 
1881 stroke of \texttt{Auto_tac} or \texttt{Force_tac}. 
1884 stroke of \texttt{Auto_tac} or \texttt{Force_tac}. Most of the time, plain 

1885 \texttt{Simp_tac} should be sufficient, though. 
1882 
1886 
1883 
1887 
1884 \section{Datatype definitions} 
1888 \section{Datatype definitions} 
1885 \label{sec:HOL:datatype} 
1889 \label{sec:HOL:datatype} 
1886 \index{*datatype(} 
1890 \index{*datatype(} 