1.1 --- a/doc-src/TutorialI/Recdef/simplification.thy	Tue Dec 11 17:07:45 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Recdef/simplification.thy	Wed Dec 12 09:04:20 2001 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  text{*\noindent
     1.5  According to the measure function, the second argument should decrease with
     1.6  each recursive call. The resulting termination condition
     1.7 -@{term[display]"n ~= 0 ==> m mod n < n"}
     1.8 +@{term[display]"n ~= (0::nat) ==> m mod n < n"}
     1.9  is proved automatically because it is already present as a lemma in
    1.10  HOL\@.  Thus the recursion equation becomes a simplification
    1.11  rule. Of course the equation is nonterminating if we are allowed to unfold
    1.12 @@ -58,7 +58,7 @@
    1.13  
    1.14  text{*\noindent
    1.15  The order of equations is important: it hides the side condition
    1.16 -@{prop"n ~= 0"}.  Unfortunately, in general the case distinction
    1.17 +@{prop"n ~= (0::nat)"}.  Unfortunately, in general the case distinction
    1.18  may not be expressible by pattern matching.
    1.19  
    1.20  A simple alternative is to replace @{text if} by @{text case},