1.1 --- a/doc-src/TutorialI/Recdef/simplification.thy	Fri Aug 04 23:02:11 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/simplification.thy	Sun Aug 06 15:26:53 2000 +0200
     1.3 @@ -18,11 +18,9 @@
     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 -*}
     1.8 -
     1.9 -(*<*)term(*>*) "n \\<noteq> 0 \\<Longrightarrow> m mod n < n";
    1.10 -
    1.11 -text{*\noindent
    1.12 +\begin{quote}
    1.13 +@{term[display]"n ~= 0 ==> m mod n < n"}
    1.14 +\end{quote}
    1.15  is provded automatically because it is already present as a lemma in the
    1.16  arithmetic library. Thus the recursion equation becomes a simplification
    1.17  rule. Of course the equation is nonterminating if we are allowed to unfold
    1.18 @@ -31,26 +29,21 @@
    1.19  something else which leads to the same problem: it splits \isa{if}s if the
    1.20  condition simplifies to neither \isa{True} nor \isa{False}. For
    1.21  example, simplification reduces
    1.22 -*}
    1.23 -
    1.24 -(*<*)term(*>*) "gcd(m,n) = k";
    1.25 -
    1.26 -text{*\noindent
    1.27 +\begin{quote}
    1.28 +@{term[display]"gcd(m,n) = k"}
    1.29 +\end{quote}
    1.30  in one step to
    1.31 -*}
    1.32 -
    1.33 -(*<*)term(*>*) "(if n=0 then m else gcd(n, m mod n)) = k";
    1.34 -
    1.35 -text{*\noindent
    1.36 +\begin{quote}
    1.37 +@{term[display]"(if n=0 then m else gcd(n, m mod n)) = k"}
    1.38 +\end{quote}
    1.39  where the condition cannot be reduced further, and splitting leads to
    1.40 -*}
    1.41 -
    1.42 -(*<*)term(*>*) "(n=0 \\<longrightarrow> m=k) \\<and> (n\\<noteq>0 \\<longrightarrow> gcd(n, m mod n)=k)";
    1.43 -
    1.44 -text{*\noindent
    1.45 -Since the recursive call \isa{gcd(n, m mod n)} is no longer protected by
    1.46 -an \isa{if}, it is unfolded again, which leads to an infinite chain of simplification steps.
    1.47 -Fortunately, this problem can be avoided in many different ways.
    1.48 +\begin{quote}
    1.49 +@{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
    1.50 +\end{quote}
    1.51 +Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
    1.52 +an \isa{if}, it is unfolded again, which leads to an infinite chain of
    1.53 +simplification steps. Fortunately, this problem can be avoided in many
    1.54 +different ways.
    1.55  
    1.56  The most radical solution is to disable the offending
    1.57  \isa{split_if} as shown in the section on case splits in