doc-src/TutorialI/Recdef/simplification.thy

 Note that the order of equations is important and hides the side condition
 @{prop"n ~= 0"}. Unfortunately, in general the case distinction
 may not be expressible by pattern matching.
 
 A very simple alternative is to replace @{text if} by @{text case}, which
-is also available for @{typ"bool"} but is not split automatically:
+is also available for @{typ bool} but is not split automatically:
 *}
 
 consts gcd2 :: "nat\<times>nat \<Rightarrow> nat";
 recdef gcd2 "measure (\<lambda>(m,n).n)"
   "gcd2(m,n) = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2(n,m mod n))";