# HG changeset patch
# User nipkow
# Date 1041183091 -3600
# Node ID 731171c27be9ac904153f11153e56bbb9aea79e4
# Parent  fb78ee03c391cd376e5d7dd57572a439085179f3
*** empty log message ***

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. *}
diff -r fb78ee03c391 -r 731171c27be9 doc-src/TutorialI/IsarOverview/Isar/Logic.thy
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Sun Dec 29 08:56:24 2002 +0100
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Sun Dec 29 18:31:31 2002 +0100
@@ -373,7 +373,7 @@
 qed
 text{*\noindent Explicit $\exists$-elimination as seen above can become
 cumbersome in practice.  The derived Isar language element
-\isakeyword{obtain} provides a more appealing form of generalized
+\isakeyword{obtain} provides a more appealing form of generalised
 existence reasoning: *}
 
 lemma assumes Pf: "\<exists>x. P(f x)" shows "\<exists>y. P y"
@@ -536,7 +536,7 @@
 important in Isar and distinguishes it from tactic-style proofs:
 \begin{quote}\em
 Do not manipulate the proof state into a particular form by applying
-tactics but state the desired form explictly and let the tactic verify
+tactics but state the desired form explicitly and let the tactic verify
 that from this form the original goal follows.
 \end{quote}
 This yields more readable and also more robust proofs. *}