diff -r 4536782969fa -r c39f83d8daeb CookBook/Package/Ind_Examples.thy
--- a/CookBook/Package/Ind_Examples.thy	Sat Feb 14 16:09:04 2009 +0000
+++ b/CookBook/Package/Ind_Examples.thy	Sun Feb 15 18:58:21 2009 +0000
@@ -5,8 +5,8 @@
 section{* Examples of Inductive Definitions \label{sec:ind-examples} *}
 
 text {*
-  Let us first give three examples showing how to define by hand inductive
-  predicates and then also how to prove by hand characteristic properties
+  Let us first give three examples showing how to define inductive
+  predicates by hand and then also how to prove by hand characteristic properties
   about them, such as introduction rules and induction principles. From
   these examples, we will figure out a general method for defining inductive
   predicates.  The aim in this section is \emph{not} to write proofs that are as
@@ -66,7 +66,7 @@
 text {*
   The proofs for the introduction are slightly more complicated. We need to prove
   the facs @{prop "trcl R x x"} and @{prop "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}.
-  In order to prove the first goal, we again unfold the definition and
+  In order to prove the first fact, we again unfold the definition and
   then apply the introdution rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible.
   We then end up in the goal state:
 *}
@@ -270,7 +270,7 @@
   and the implication in the premise. We first convert the meta-level universal quantifier
   and implication to their object-level counterparts. Unfolding the definition of
   @{text accpart} and applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}
-  yields the following proof state:
+  yields the following goal state:
 *}
 
 (*<*)lemma accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
@@ -280,7 +280,7 @@
 (*<*)oops(*>*)
 
 text {*
-  Applying the second assumption produces a proof state with the new local assumption
+  Applying the second assumption produces a goal state with the new local assumption
   @{term "R y x"}, which will then be used to solve the goal @{term "P y"} using the
   first assumption.
 *}