--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Apr 14 17:50:22 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Apr 14 19:46:36 2010 +0200
@@ -471,7 +471,7 @@
Note that the resulting simplification and induction rules
correspond to the transformed specification, not the one given
originally. This usually means that each equation given by the user
- may result in several theroems. Also note that this automatic
+ may result in several theorems. Also note that this automatic
transformation only works for ML-style datatype patterns.
\item @{text domintros} enables the automated generation of