diff -r 449e1a1bb7a8 -r d848c6693185 doc-src/TutorialI/Inductive/AB.thy
--- a/doc-src/TutorialI/Inductive/AB.thy	Fri Feb 16 00:36:21 2001 +0100
+++ b/doc-src/TutorialI/Inductive/AB.thy	Fri Feb 16 06:46:20 2001 +0100
@@ -105,7 +105,7 @@
 @{text"\<bar>.\<bar>"} is the absolute value function, and @{term"#1::int"} is the
 integer 1 (see \S\ref{sec:numbers}).
 
-First we show that the our specific function, the difference between the
+First we show that our specific function, the difference between the
 numbers of @{term a}'s and @{term b}'s, does indeed only change by 1 in every
 move to the right. At this point we also start generalizing from @{term a}'s
 and @{term b}'s to an arbitrary property @{term P}. Otherwise we would have
@@ -119,7 +119,7 @@
 
 txt{*\noindent
 The lemma is a bit hard to read because of the coercion function
-@{term[source]"int :: nat \<Rightarrow> int"}. It is required because @{term size} returns
+@{text"int :: nat \<Rightarrow> int"}. It is required because @{term size} returns
 a natural number, but subtraction on type~@{typ nat} will do the wrong thing.
 Function @{term take} is predefined and @{term"take i xs"} is the prefix of
 length @{term i} of @{term xs}; below we also need @{term"drop i xs"}, which
@@ -237,7 +237,7 @@
 txt{*\noindent
 This yields an index @{prop"i \<le> length v"} such that
 @{prop[display]"length [x\<in>take i v . x = a] = length [x\<in>take i v . x = b] + 1"}
-With the help of @{thm[source]part1} it follows that
+With the help of @{thm[source]part2} it follows that
 @{prop[display]"length [x\<in>drop i v . x = a] = length [x\<in>drop i v . x = b] + 1"}
 *}
 
@@ -287,18 +287,20 @@
 grammar, for no good reason, excludes the empty word.  That complicates
 matters just a little bit because we now have 8 instead of our 7 productions.
 
-More importantly, the proof itself is different: rather than separating the
-two directions, they perform one induction on the length of a word. This
-deprives them of the beauty of rule induction and in the easy direction
-(correctness) their reasoning is more detailed than our @{text auto}. For the
-hard part (completeness), they consider just one of the cases that our @{text
-simp_all} disposes of automatically. Then they conclude the proof by saying
-about the remaining cases: ``We do this in a manner similar to our method of
-proof for part (1); this part is left to the reader''. But this is precisely
-the part that requires the intermediate value theorem and thus is not at all
-similar to the other cases (which are automatic in Isabelle). We conclude
-that the authors are at least cavalier about this point and may even have
-overlooked the slight difficulty lurking in the omitted cases. This is not
-atypical for pen-and-paper proofs, once analysed in detail.  *}
+More importantly, the proof itself is different: rather than
+separating the two directions, they perform one induction on the
+length of a word. This deprives them of the beauty of rule induction,
+and in the easy direction (correctness) their reasoning is more
+detailed than our @{text auto}. For the hard part (completeness), they
+consider just one of the cases that our @{text simp_all} disposes of
+automatically. Then they conclude the proof by saying about the
+remaining cases: ``We do this in a manner similar to our method of
+proof for part (1); this part is left to the reader''. But this is
+precisely the part that requires the intermediate value theorem and
+thus is not at all similar to the other cases (which are automatic in
+Isabelle). The authors are at least cavalier about this point and may
+even have overlooked the slight difficulty lurking in the omitted
+cases. This is not atypical for pen-and-paper proofs, once analysed in
+detail.  *}
 
 (*<*)end(*>*)