--- 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. *}
--- 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. *}