--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Fri Jun 13 20:57:26 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Fri Jun 13 20:57:51 2008 +0200
@@ -4,7 +4,7 @@
datatype nat = Suc of nat | Zero_nat;
fun eq_nat Zero_nat Zero_nat = true
- | eq_nat (Suc m) (Suc n) = eq_nat m n
+ | eq_nat (Suc nat) (Suc nat') = eq_nat nat nat'
| eq_nat Zero_nat (Suc a) = false
| eq_nat (Suc a) Zero_nat = false;
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Fri Jun 13 20:57:26 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Fri Jun 13 20:57:51 2008 +0200
@@ -29,7 +29,7 @@
datatype nat = Suc of nat | Zero_nat;
fun eq_nat Zero_nat Zero_nat = true
- | eq_nat (Suc m) (Suc n) = eq_nat m n
+ | eq_nat (Suc nat) (Suc nat') = eq_nat nat nat'
| eq_nat Zero_nat (Suc a) = false
| eq_nat (Suc a) Zero_nat = false;
--- a/doc-src/TutorialI/Inductive/document/Star.tex Fri Jun 13 20:57:26 2008 +0200
+++ b/doc-src/TutorialI/Inductive/document/Star.tex Fri Jun 13 20:57:51 2008 +0200
@@ -131,7 +131,7 @@
depend on its second parameter at all. The reason is that in our original
goal, of the pair \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}} only \isa{x} appears also in the
conclusion, but not \isa{y}. Thus our induction statement is too
-weak. Fortunately, it can easily be strengthened:
+general. Fortunately, it can easily be specialized:
transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:%
\end{isamarkuptxt}%
\isamarkuptrue%