diff -r b7d96e94796f -r ff003e2b790c doc-src/TutorialI/Inductive/AB.thy
--- a/doc-src/TutorialI/Inductive/AB.thy	Fri Oct 20 13:15:26 2000 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy	Fri Oct 20 14:17:08 2000 +0200
@@ -74,7 +74,7 @@
 
 txt{*\noindent
 These propositions are expressed with the help of the predefined @{term
-filter} function on lists, which has the convenient syntax @{term"[x\<in>xs. P
+filter} function on lists, which has the convenient syntax @{text"[x\<in>xs. P
 x]"}, the list of all elements @{term x} in @{term xs} such that @{prop"P x"}
 holds. Remember that on lists @{term size} and @{term length} are synonymous.
 
@@ -97,8 +97,8 @@
 following little lemma: every string with two more @{term a}'s than @{term
 b}'s can be cut somehwere such that each half has one more @{term a} than
 @{term b}. This is best seen by imagining counting the difference between the
-number of @{term a}'s than @{term b}'s starting at the left end of the
-word. We start at 0 and end (at the right end) with 2. Since each move to the
+number of @{term a}'s and @{term b}'s starting at the left end of the
+word. We start with 0 and end (at the right end) with 2. Since each move to the
 right increases or decreases the difference by 1, we must have passed through
 1 on our way from 0 to 2. Formally, we appeal to the following discrete
 intermediate value theorem @{thm[source]nat0_intermed_int_val}
@@ -141,7 +141,7 @@
 
 text{*
 Finally we come to the above mentioned lemma about cutting a word with two
-more elements of one sort than of the other sort into two halfs:
+more elements of one sort than of the other sort into two halves:
 *}
 
 lemma part1: