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