# HG changeset patch
# User wenzelm
# Date 1213383471 -7200
# Node ID 431f695fc86527612867ee61f04f439668b1aebe
# Parent  1a9b9da1c0d712607468ee6f65e3aa3fa41b1685
updated generated file;

diff -r 1a9b9da1c0d7 -r 431f695fc865 doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML
--- 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;
 
diff -r 1a9b9da1c0d7 -r 431f695fc865 doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML
--- 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;
 
diff -r 1a9b9da1c0d7 -r 431f695fc865 doc-src/TutorialI/Inductive/document/Star.tex
--- 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%