diff -r fb78ee03c391 -r 731171c27be9 doc-src/TutorialI/IsarOverview/Isar/Induction.thy
--- a/doc-src/TutorialI/IsarOverview/Isar/Induction.thy	Sun Dec 29 08:56:24 2002 +0100
+++ b/doc-src/TutorialI/IsarOverview/Isar/Induction.thy	Sun Dec 29 18:31:31 2002 +0100
@@ -47,7 +47,7 @@
 
 The same game can be played with other datatypes, for example lists,
 where @{term tl} is the tail of a list, and @{text length} returns a
-natual number:
+natural number:
 \Tweakskip
 *}
 (*<*)declare length_tl[simp del](*>*)
@@ -132,7 +132,7 @@
 automatically: for example in case @{text"(Suc n)"}, @{text ?case} is only
 @{prop"Q' x"} whereas the assumptions (named @{term Suc}!) contain both the
 usual induction hypothesis \emph{and} @{prop"P' x"}.
-It should be clear how this generalizes to more complex formulae.
+It should be clear how this generalises to more complex formulae.
 
 As an example we will now prove complete induction via
 structural induction. *}