doc-src/TutorialI/Recdef/termination.thy

 from them) as theorems. For example, look (via \isacommand{thm}) at
 @{thm[source]sep.simps} and @{thm[source]sep1.simps} to see that they define
 the same function. What is more, those equations are automatically declared as
 simplification rules.
 
-In general, Isabelle may not be able to prove all termination condition
+In general, Isabelle may not be able to prove all termination conditions
 (there is one for each recursive call) automatically. For example,
 termination of the following artificial function
 *}
 
 consts f :: "nat\<times>nat \<Rightarrow> nat";