doc-src/IsarRef/Thy/HOL_Specific.thy

   equations take precedence over later ones.  This allows to give the
   specification in a format very similar to functional programming.
   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
   introduction rules for the domain predicate. While mostly not
   needed, they can be helpful in some proofs about partial functions.