doc-src/TutorialI/Datatype/Fundata.thy

--- a/doc-src/TutorialI/Datatype/Fundata.thy	Fri May 18 16:45:55 2001 +0200
+++ b/doc-src/TutorialI/Datatype/Fundata.thy	Fri May 18 17:18:43 2001 +0200
@@ -32,7 +32,7 @@
 Isabelle because the termination proof is not as obvious since
 @{term"map_bt"} is only partially applied.
 
-The following lemma has a canonical proof:  *}
+The following lemma has a simple proof by induction:  *}
 
 lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
 apply(induct_tac T, simp_all)