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