1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Fri Jun 13 20:57:26 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Fri Jun 13 20:57:51 2008 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  datatype nat = Suc of nat | Zero_nat;
     1.5  
     1.6  fun eq_nat Zero_nat Zero_nat = true
     1.7 -  | eq_nat (Suc m) (Suc n) = eq_nat m n
     1.8 +  | eq_nat (Suc nat) (Suc nat') = eq_nat nat nat'
     1.9    | eq_nat Zero_nat (Suc a) = false
    1.10    | eq_nat (Suc a) Zero_nat = false;
    1.11  

     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Fri Jun 13 20:57:26 2008 +0200
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Fri Jun 13 20:57:51 2008 +0200
     2.3 @@ -29,7 +29,7 @@
     2.4  datatype nat = Suc of nat | Zero_nat;
     2.5  
     2.6  fun eq_nat Zero_nat Zero_nat = true
     2.7 -  | eq_nat (Suc m) (Suc n) = eq_nat m n
     2.8 +  | eq_nat (Suc nat) (Suc nat') = eq_nat nat nat'
     2.9    | eq_nat Zero_nat (Suc a) = false
    2.10    | eq_nat (Suc a) Zero_nat = false;
    2.11  

     3.1 --- a/doc-src/TutorialI/Inductive/document/Star.tex	Fri Jun 13 20:57:26 2008 +0200
     3.2 +++ b/doc-src/TutorialI/Inductive/document/Star.tex	Fri Jun 13 20:57:51 2008 +0200
     3.3 @@ -131,7 +131,7 @@
     3.4  depend on its second parameter at all. The reason is that in our original
     3.5  goal, of the pair \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}} only \isa{x} appears also in the
     3.6  conclusion, but not \isa{y}. Thus our induction statement is too
     3.7 -weak. Fortunately, it can easily be strengthened:
     3.8 +general. Fortunately, it can easily be specialized:
     3.9  transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:%
    3.10  \end{isamarkuptxt}%
    3.11  \isamarkuptrue%