doc-src/TutorialI/Recdef/simplification.thy

   "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))";
 
 text{*\noindent
 According to the measure function, the second argument should decrease with
 each recursive call. The resulting termination condition
-@{term[display]"n ~= 0 ==> m mod n < n"}
+@{term[display]"n ~= (0::nat) ==> m mod n < n"}
 is proved automatically because it is already present as a lemma in
 HOL\@.  Thus the recursion equation becomes a simplification
 rule. Of course the equation is nonterminating if we are allowed to unfold
 the recursive call inside the @{text else} branch, which is why programming
 languages and our simplifier don't do that. Unfortunately the simplifier does

   "gcd1 (m, n) = gcd1(n, m mod n)";
 
 
 text{*\noindent
 The order of equations is important: it hides the side condition
-@{prop"n ~= 0"}.  Unfortunately, in general the case distinction
+@{prop"n ~= (0::nat)"}.  Unfortunately, in general the case distinction
 may not be expressible by pattern matching.
 
 A simple alternative is to replace @{text if} by @{text case}, 
 which is also available for @{typ bool} and is not split automatically:
 *}