--- a/CookBook/Package/Ind_Prelims.thy	Sat Feb 21 11:38:14 2009 +0000
+++ b/CookBook/Package/Ind_Prelims.thy	Sun Feb 22 03:44:03 2009 +0000
@@ -5,11 +5,11 @@
 section{* Preliminaries *}
   
 text {*
-  On the Isabelle level, the user will just give a specification of an
-  inductive predicate and expects from the package to produce a convenient
-  reasoning infrastructure. This infrastructure needs to be derived from the 
-  definition that correspond to the specified predicate. This will roughly 
-  mean that the package has three main parts, namely:
+  The user will just give a specification of an inductive predicate and
+  expects from the package to produce a convenient reasoning
+  infrastructure. This infrastructure needs to be derived from the definition
+  that correspond to the specified predicate. This will roughly mean that the
+  package has three main parts, namely:
 
 
   \begin{itemize}
@@ -18,13 +18,14 @@
   \item storing the results in the theory. 
   \end{itemize}
 
-  Before we start with explaining all parts,
-  let us first give three examples showing how to define inductive predicates
-  by hand and then also how to prove by hand important properties about
-  them. 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 beautiful as possible, but as close as possible to the ML-code
-  we will develop in later sections.
+  Before we start with explaining all parts, let us first give three examples
+  showing how to define inductive predicates by hand and then also how to
+  prove by hand important properties about them. 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 beautiful as
+  possible, but as close as possible to the ML-code we will develop in later
+  sections.
+
 
   We first consider the transitive closure of a relation @{text R}. It is
   an inductive predicate characterised by the two introduction rules:
@@ -34,7 +35,7 @@
   @{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}
   \end{center}
 
-  In Isabelle the user will state for @{term trcl\<iota>} the specification:
+  In Isabelle, the user will state for @{term trcl\<iota>} the specification:
 *}
 
 simple_inductive
@@ -65,7 +66,7 @@
   reasoning for the user.
 
   With this definition, the proof of the induction principle for @{term trcl}
-  closure is almost immediate. It suffices to convert all the meta-level
+  is almost immediate. It suffices to convert all the meta-level
   connectives in the lemma to object-level connectives using the
   proof method @{text atomize} (Line 4), expand the definition of @{term trcl}
   (Line 5 and 6), eliminate the universal quantifier contained in it (Line~7),
@@ -203,8 +204,8 @@
  
   \begin{center}\small
   @{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm}
-  @{prop[mode=Rule] "odd m \<Longrightarrow> even (Suc m)"} \hspace{5mm}
-  @{prop[mode=Rule] "even m \<Longrightarrow> odd (Suc m)"}
+  @{prop[mode=Rule] "odd n \<Longrightarrow> even (Suc n)"} \hspace{5mm}
+  @{prop[mode=Rule] "even n \<Longrightarrow> odd (Suc n)"}
   \end{center}
   
   The user will state for this inductive definition the specification:
@@ -339,13 +340,13 @@
 text {*
   In Line 11, applying the assumption @{text "r1"} generates a goal state with
   the new local assumption @{term "R y x"}, named @{text "r1_prem"} in the 
-  proof above (Line 14). This local assumption will be used to solve
-  the goal @{term "P y"} using the assumption @{text "p1"}.
+  proof above (Line 14). This local assumption is used to solve
+  the goal @{term "P y"} with the help of assumption @{text "p1"}.
 
   The point of these examples is to get a feeling what the automatic proofs 
   should do in order to solve all inductive definitions we throw at them.
-  This is usually the first step in writing a package.
+  This is usually the first step in writing a package. We next explain
+  the parsing and typing part of the package.
 
 *}
-
-end
+(*<*)end(*>*)