doc-src/IsarRef/Thy/HOL_Specific.thy
 changeset 36139 0c2538afe8e8 parent 35841 94f901e4969a child 36158 d2ad76e374d3
     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