--- a/Admin/isatest/isatest-settings Sun Feb 15 22:58:02 2009 +0100
+++ b/Admin/isatest/isatest-settings Mon Feb 16 10:15:43 2009 +0100
@@ -11,7 +11,7 @@
HOME=/home/isatest
## send email on failure to
-MAILTO="kleing@cse.unsw.edu.au nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk makarius@sketis.net haftmann@in.tum.de krauss@in.tum.de"
+MAILTO="kleing@cse.unsw.edu.au nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk makarius@sketis.net haftmann@in.tum.de krauss@in.tum.de blanchet@in.tum.de"
LOGPREFIX=$HOME/log
MASTERLOG=$LOGPREFIX/isatest.log
--- a/src/HOL/List.thy Sun Feb 15 22:58:02 2009 +0100
+++ b/src/HOL/List.thy Mon Feb 16 10:15:43 2009 +0100
@@ -257,7 +257,7 @@
\caption{Characteristic examples}
\label{fig:Characteristic}
\end{figure}
-Figure~\ref{fig:Characteristic} shows charachteristic examples
+Figure~\ref{fig:Characteristic} shows characteristic examples
that should give an intuitive understanding of the above functions.
*}
--- a/src/HOL/Tools/datatype_abs_proofs.ML Sun Feb 15 22:58:02 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Mon Feb 16 10:15:43 2009 +0100
@@ -262,7 +262,8 @@
in
thy2
|> Sign.add_path (space_implode "_" new_type_names)
- |> PureThy.add_thmss [((Binding.name "recs", rec_thms), [])]
+ |> PureThy.add_thmss [((Binding.name "recs", rec_thms),
+ [Nitpick_Const_Simp_Thms.add])]
||> Sign.parent_path
||> Theory.checkpoint
|-> (fn thms => pair (reccomb_names, Library.flat thms))