--- a/ProgTutorial/Package/Ind_Code.thy	Fri Mar 27 12:49:28 2009 +0000
+++ b/ProgTutorial/Package/Ind_Code.thy	Fri Mar 27 18:19:42 2009 +0000
@@ -5,9 +5,9 @@
 section {* The Gory Details\label{sec:code} *} 
 
 text {*
-  As mentioned before the code falls roughly into three parts: the definitions,
-  the induction principles and the introduction rules. In addition there is an 
-  administrative function that strings everything together. 
+  As mentioned before the code falls roughly into three parts: code that deals 
+  with the definitions, the induction principles and the introduction rules, respectively. 
+  In addition there are some administrative functions that string everything together. 
 *}
 
 subsection {* Definitions *}
@@ -236,22 +236,22 @@
 text {*
   This helper function instantiates the @{text "?x"} in the theorem 
   @{thm spec} with a given @{ML_type cterm}. We call this helper function
-  in the next tactic, called @{text inst_spec_tac}.
+  in the following tactic, called @{text inst_spec_tac}.
 *}
 
 ML{*fun inst_spec_tac ctrms = 
   EVERY' (map (dtac o inst_spec) ctrms)*}
 
 text {*
-  This tactic expects a list of @{ML_type cterm}s. It allows us in the following 
-  proof to instantiate the three quantifiers in the assumption. 
+  This tactic expects a list of @{ML_type cterm}s. It allows us in the 
+  proof below to instantiate the three quantifiers in the assumption. 
 *}
 
 lemma 
   fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
   shows "\<forall>x y z. P x y z \<Longrightarrow> True"
 apply (tactic {* 
-  inst_spec_tac  [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *})
+  inst_spec_tac [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *})
 txt {* 
   We obtain the goal state
 
@@ -311,8 +311,8 @@
   The variables @{text "z"}, @{text "P"} and @{text "Q"} are schematic
   variables (since they are not quantified in the lemma). These schematic
   variables are needed so that they can be instantiated by the user. 
-  We have to take care to also generate these schematic variables when
-  generating the goals for the induction principles.  In general we have 
+  It will take a bit of work to generate these schematic variables when
+  constructing the goals for the induction principles.  In general we have 
   to construct for each predicate @{text "pred"} a goal of the form
 
   @{text [display] 
@@ -321,9 +321,9 @@
   where the predicates @{text preds} are replaced in @{text rules} by new 
   distinct variables @{text "?Ps"}. We also need to generate fresh arguments 
   @{text "?zs"} for the predicate  @{text "pred"} and the @{text "?P"} in 
-  the conclusion. The crucial point is that the  @{text "?Ps"} and 
-  @{text "?zs"} need to be schematic variables that can be instantiated 
-  by the user.
+  the conclusion. As just mentioned, the crucial point is that the  
+  @{text "?Ps"} and @{text "?zs"} need to be schematic variables that can 
+  be instantiated by the user.
 
   We generate these goals in two steps. The first function, named @{text prove_ind}, 
   expects that the introduction rules are already appropriately substituted. The argument
@@ -352,16 +352,17 @@
 text {* 
   In Line 3 we produce names @{text "zs"} for each type in the 
   argument type list. Line 4 makes these names unique and declares them as 
-  \emph{free} (but fixed) variables in the local theory @{text "lthy'"}. 
-  That means they are not (yet) schematic variables.
+  \emph{free but fixed} variables in the local theory @{text "lthy'"}. 
+  That means they are not schematic variables (yet).
   In Line 5 we construct the terms corresponding to these variables. 
   The variables are applied to the predicate in Line 7 (this corresponds
   to the first premise @{text "pred zs"} of the induction principle). 
   In Line 8 and 9, we first construct the term  @{text "P zs"} 
-  and then add the (substituted) introduction rules as premises. In case that
-  no introduction rules are given, the conclusion of this implication needs
-  to be wrapped inside a @{term Trueprop}, otherwise the Isabelle's goal
-  mechanism will fail. 
+  and then add the (substituted) introduction rules as preconditions. In 
+  case that no introduction rules are given, the conclusion of this 
+  implication needs to be wrapped inside a @{term Trueprop}, otherwise 
+  the Isabelle's goal mechanism will fail.\footnote{FIXME: check with 
+  Stefan...is this so?} 
 
   In Line 11 we set up the goal to be proved; in the next line we call the
   tactic for proving the induction principle. As mentioned before, this tactic
@@ -467,18 +468,25 @@
 subsection {* Introduction Rules *}
 
 text {*
-  The proofs of the introduction rules are quite a bit
-  more involved than the ones for the induction principles. 
-  To ease somewhat our work here, we use the following two helper
-  functions.
+  Constructing the goals for the introduction rules is easy: they
+  are just the rules given by the user. However, their proofs are 
+  quite a bit more involved than the ones for the induction principles. 
+  To explain the general method, our running example will be
+  the introduction rule
 
+  \begin{isabelle}
+  @{prop "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"}
+  \end{isabelle}
+  
+  about freshness for lambdas. In order to ease somewhat 
+  our work here, we use the following two helper functions.
 *}
 
 ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct)
 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*}
 
 text {* 
-  To see what these functions do, let us suppose whe have the following three
+  To see what these functions do, let us suppose we have the following three
   theorems. 
 *}
 
@@ -515,14 +523,7 @@
             (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"
   "C"}
 
-  To explain the proof for the introduction rule, our running example will be
-  the rule:
-
-  \begin{isabelle}
-  @{prop "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"}
-  \end{isabelle}
-  
-  for freshness of applications. We set up the proof as follows:
+  Now we set up the proof for the introduction rule as follows:
 *}
 
 lemma fresh_Lam:
@@ -530,19 +531,19 @@
 (*<*)oops(*>*)
 
 text {*
-  The first step will be to expand the definitions of freshness
+  The first step in the proof will be to expand the definitions of freshness
   and then introduce quantifiers and implications. For this we
   will use the tactic
 *}
 
-ML{*fun expand_tac defs =
+ML %linenosgray{*fun expand_tac defs =
   ObjectLogic.rulify_tac 1
   THEN rewrite_goals_tac defs
   THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *}
 
 text {*
-  The first step of ``rulifying'' the lemma will turn out to be important
-  later on. Applying this tactic 
+  The function in Line 2 ``rulifies'' the lemma. This will turn out to 
+  be important later on. Applying this tactic 
 *}
 
 (*<*)
@@ -562,20 +563,20 @@
   and @{text "t"}) which come from the introduction rule and parameters
   (in the case above only @{text "fresh"}) which come from the universal
   quantification in the definition @{term "fresh a (App t s)"}.
-  Similarly, there are preconditions
-  that come from the premises of the rule and premises from the
-  definition. We need to treat these 
-  parameters and preconditions differently. In the code below
+  Similarly, there are assumptions
+  that come from the premises of the rule and assumptions from the
+  definition of the predicate. We need to treat these 
+  parameters and assumptions differently. In the code below
   we will therefore separate them into @{text "params1"} and @{text params2},
   respectively @{text "prems1"} and @{text "prems2"}. To do this 
   separation, it is best to open a subproof with the tactic 
   @{ML SUBPROOF}, since this tactic provides us
-  with the parameters (as list of @{ML_type cterm}s) and the premises
-  (as list of @{ML_type thm}s). The problem we have to overcome 
-  with @{ML SUBPROOF} is, however, that this tactic always expects us to completely 
-  discharge the goal (see Section~\ref{sec:simpletacs}). This is inconvenient for
-  our gradual explanation of the proof here. To circumvent this inconvenience
-  we use the following modified tactic: 
+  with the parameters (as list of @{ML_type cterm}s) and the assumptions
+  (as list of @{ML_type thm}s called @{text prems}). The problem we have 
+  to overcome with @{ML SUBPROOF} is, however, that this tactic always 
+  expects us to completely discharge the goal (see Section~\ref{sec:simpletacs}). 
+  This is inconvenient for our gradual explanation of the proof here. To 
+  circumvent this inconvenience we use the following modified tactic: 
 *}
 (*<*)oops(*>*)
 ML{*fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac*}
@@ -583,7 +584,8 @@
 text {*
   If the tactic inside @{ML SUBPROOF} fails, then the overall tactic will
   still succeed. With this testing tactic, we can gradually implement
-  all necessary proof steps inside a subproof.
+  all necessary proof steps inside a subproof. Once we are finished, we
+  just have to replace it with @{ML SUBPROOF}.
 *}
 
 text_raw {*
@@ -612,8 +614,8 @@
 
 text {*
   First we calculate the values for @{text "params1/2"} and @{text "prems1/2"}
-  from @{text "params"} and @{text "prems"}, respectively. To see what is
-  going in our example, we will print out the values using the printing
+  from @{text "params"} and @{text "prems"}, respectively. To better see what is
+  going in our example, we will print out these values using the printing
   function in Figure~\ref{fig:chopprint}. Since the tactic @{ML SUBPROOF} will
   supply us the @{text "params"} and @{text "prems"} as lists, we can 
   separate them using the function @{ML chop}. 
@@ -629,9 +631,10 @@
   end) *}
 
 text {* 
-  For the separation we can rely on that Isabelle deterministically 
-  produces parameter and premises in a goal state. The last parameters
-  that were introduced come from the quantifications in the definitions.
+  For the separation we can rely on the fact that Isabelle deterministically 
+  produces parameters and premises in a goal state. The last parameters
+  that were introduced come from the quantifications in the definitions
+  (see the tactic @{ML expand_tac}).
   Therefore we only have to subtract the number of predicates (in this
   case only @{text "1"}) from the lenghts of all parameters. Similarly
   with the @{text "prems"}: the last premises in the goal state come from 
@@ -675,7 +678,7 @@
   We now have to select from @{text prems2} the premise 
   that corresponds to the introduction rule we prove, namely:
 
-  @{term [display] "\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)"}
+  @{term [display] "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam a t)"}
 
   To use this premise with @{ML rtac}, we need to instantiate its 
   quantifiers (with @{text params1}) and transform it into rule 
@@ -683,7 +686,7 @@
   subproof as follows:
 *}
 
-ML{*fun apply_prem_tac i preds rules =
+ML %linenosgray{*fun apply_prem_tac i preds rules =
   SUBPROOF_test (fn {params, prems, context, ...} =>
   let
     val (params1, params2) = chop (length params - length preds) params
@@ -696,9 +699,9 @@
 
 text {* 
   The argument @{text i} corresponds to the number of the 
-  introduction we want to analyse. We will later on lat it range
-  from @{text 0} to the number of introduction rules.
-  Below we applying this function with @{text 3}, since 
+  introduction we want to prove. We will later on lat it range
+  from @{text 0} to the number of @{text "rules - 1"}.
+  Below we apply this function with @{text 3}, since 
   we are proving the fourth introduction rule. 
 *}
 
@@ -712,19 +715,19 @@
 
 text {*
   Since we print out the goal state just after the application of 
-  @{ML rtac}, we can see the goal state we obtain: as expected it has 
-  the two subgoals
+  @{ML rtac} (Line 8), we can see the goal state we obtain: 
 
   \begin{isabelle}
   @{text "1."}~@{prop "a \<noteq> b"}\\
   @{text "2."}~@{prop "fresh a t"}
   \end{isabelle}
 
-  where the first comes from a non-recursive premise of the rule
-  and the second comes from a recursive premise. The first goal
-  can be solved immediately by @{text "prems1"}. The second
-  needs more work. It can be solved with the other premise 
-  in @{text "prems1"}, namely
+  As expected there are two subgoals, where the first comes from a
+  non-recursive premise of the introduction rule and the second comes 
+  from a recursive premise. The first goal can be solved immediately 
+  by @{text "prems1"}. The second needs more work. It can be solved 
+  with the other premise in @{text "prems1"}, namely
+
 
   @{term [break,display]
   "\<forall>fresh.
@@ -737,8 +740,8 @@
   come from @{text "params1"} and @{text "prems2"}. We can determine
   whether we are in the simple or complicated case by checking whether
   the topmost connective is an @{text "\<forall>"}. The premises in the simple
-  case cannot have such a quantification, since in the first step 
-  of @{ML "expand_tac"} was the ``rulification'' of the lemma. 
+  case cannot have such a quantification, since the first step 
+  of @{ML "expand_tac"} was to ``rulify'' the lemma. 
   The premise of the complicated case must have at least one  @{text "\<forall>"}
   coming from the quantification over the @{text preds}. So 
   we can implement the following function
@@ -769,6 +772,7 @@
   end) *}
 
 text {*
+  Note that the tactic is now @{ML SUBPROOF}, not @{ML SUBPROOF_test}. 
   The full proof of the introduction rule now as follows:
 *}
 
@@ -779,10 +783,10 @@
 done
 
 text {* 
-  Unfortunately, not everything is done yet. If you look closely
-  at the general principle outlined in Section~\ref{sec:nutshell}, 
-  we have  not yet dealt with the case when recursive premises 
-  in a rule have preconditions @{text Bs}. The introduction rule
+  Phew!  Unfortunately, not everything is done yet. If you look closely
+  at the general principle outlined for the introduction rules in 
+  Section~\ref{sec:nutshell}, we have  not yet dealt with the case where 
+  recursive premises have preconditions. The introduction rule
   of the accessible part is such a rule. 
 *}
 
@@ -818,10 +822,10 @@
 *}(*<*)oops(*>*)
 
 text {*
-  In order to make progress as before, we have to use the precondition
+  In order to make progress, we have to use the precondition
   @{text "R y x"} (in general there can be many of them). The best way
   to get a handle on these preconditions is to open up another subproof,
-  since the preconditions will be bound to @{text prems}. Therfore we
+  since the preconditions will then be bound to @{text prems}. Therfore we
   modify the function @{ML prepare_prem} as follows
 *}
 
@@ -839,13 +843,17 @@
 
 text {*
   In Line 4 we use the @{text prems} from the @{ML SUBPROOF} and resolve 
-  them with @{text prem}. In the simple case, that is where the @{text prem} 
+  them with @{text prem}. In the simple cases, that is where the @{text prem} 
   comes from a non-recursive premise of the rule, @{text prems} will be 
-  just the empty list and the @{ML MRS} does nothing. Similarly, in the 
+  just the empty list and the function @{ML MRS} does nothing. Similarly, in the 
   cases where the recursive premises of the rule do not have preconditions. 
+  In case there are preconditions, then Line 4 discharges them. After
+  that we can proceed as before, i.e., check whether the outermost
+  connective is @{text "\<forall>"}.
   
-  The function @{ML prove_intro_tac} only needs to give the context to
-  @{ML prepare_prem} (Line 8) and is as follows.
+  The function @{ML prove_intro_tac} only needs to be changed so that it
+  gives the context to @{ML prepare_prem} (Line 8). The modified version
+  is below.
 *}
 
 ML %linenosgray{*fun prove_intro_tac i preds rules =
@@ -859,7 +867,7 @@
   end) *}
 
 text {*
-  With these extended function we can also prove the introduction
+  With these two functions we can now also prove the introduction
   rule for the accessible part. 
 *}
 
@@ -882,14 +890,13 @@
 
 text {*
   Lines 2 to 4 correspond to the function @{ML expand_tac}. Some testcases
-  dor this tactic are:
+  for this tactic are:
 *}
 
 lemma even0_intro:
   shows "even 0"
 by (tactic {* intro_tac eo_defs eo_rules eo_preds 0 @{context} *})
 
-
 lemma evenS_intro:
   shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"
 by (tactic {* intro_tac eo_defs eo_rules eo_preds 1 @{context} *})
@@ -900,9 +907,10 @@
   intro_tac @{thms fresh_def} fresh_rules [fresh_pred] 1 @{context} *})
 
 text {*
-  The second function sets up in Line 4 the goals (in this case this is easy
-  since they are exactly the introduction rules the user gives)
-  and iterates @{ML intro_tac} over all introduction rules.
+  The second function sets up in Line 4 the goals (this is easy
+  for the introduction rules since they are exactly the rules 
+  given by the user) and iterates @{ML intro_tac} over all 
+  introduction rules.
 *}
 
 ML %linenosgray{*fun intros rules preds defs lthy = 
@@ -914,6 +922,14 @@
   map_index intros_aux rules
 end*}
 
+text {*
+  The iteration is done with the function @{ML map_index} since we
+  need the introduction rule together with its number (counted from
+  @{text 0}). This completes the code for the functions deriving the
+  reasoning infrastructure. It remains to implement some administrative
+  code that strings everything together.
+*}
+
 subsection {* Main Function *}
 
 text {* main internal function *}

--- a/ProgTutorial/Package/Ind_General_Scheme.thy	Fri Mar 27 12:49:28 2009 +0000
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy	Fri Mar 27 18:19:42 2009 +0000
@@ -20,23 +20,15 @@
 section {* The Code in a Nutshell\label{sec:nutshell} *}
 
 text {*
-  (FIXME: perhaps move somewhere else)
-
-  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. For this 
-  it is instructive to look at the general construction principle 
-  of inductive definitions, which we shall do in the next section.
-*}
-
-text {*
-  The inductive package will generate the reasoning infrastructure
-  for mutually recursive predicates @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what
-  follows we will have the convention that various, possibly empty collections of 
-  ``things'' are indicated either by adding an @{text "s"} or by adding 
-  a superscript @{text [quotes] "\<^isup>*"}. The shorthand for the predicates 
-  will therefore be @{text "preds"} or @{text "pred\<^sup>*"}. In the case of the
-  predicates there must be, of course, at least a single one in order to obtain a 
-  meaningful definition.
+  The inductive package will generate the reasoning infrastructure for
+  mutually recursive predicates @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what
+  follows we will have the convention that various, possibly empty collections
+  of ``things'' (lists, nested implications and so on) are indicated either by
+  adding an @{text [quotes] "s"} or by adding a superscript @{text [quotes]
+  "\<^isup>*"}. The shorthand for the predicates will therefore be @{text
+  "preds"} or @{text "pred\<^sup>*"}. In the case of the predicates there must
+  be, of course, at least a single one in order to obtain a meaningful
+  definition.
 
   The input for the inductive package will be some @{text "preds"} with possible 
   typing and syntax annotations, and also some introduction rules. We call below the 
@@ -54,11 +46,11 @@
   this format and omit any code that actually tests this. Therefore ``things'' 
   can go horribly wrong, if the @{text "rules"} are not of this
   form.\footnote{FIXME: Exercise to test this format.} The @{text As} and
-  @{text Bs} in a @{text "rule"} are formulae not involving the inductive
+  @{text Bs} in a @{text "rule"} stand for formulae not involving the inductive
   predicates @{text "preds"}; the instances @{text "pred ss"} and @{text "pred
   ts"} can stand for different predicates, like @{text "pred\<^isub>1 ss"} and 
   @{text "pred\<^isub>2 ts"}; @{text ss} and @{text ts} are the
-  arguments of the predicates. Every formula left of @{text [quotes]
+  arguments of these predicates. Every formula left of @{text [quotes]
   "\<Longrightarrow> pred ts"} is a premise of the rule. The outermost quantified 
   variables @{text "xs"} are usually omitted in the user's input. The 
   quantification for the variables @{text "ys"} is local with respect to 
@@ -75,7 +67,7 @@
 
   @{thm [display] accpartI[no_vars]}
 
-  has a recursive premise that has a precondition. As usual all 
+  has a single recursive premise that has a precondition. As usual all 
   rules are stated without the leading meta-quantification @{text "\<And>xs"}.
 
   The code of the inductive package falls roughly in tree parts: the first
@@ -106,11 +98,12 @@
 
   @{text [display] "pred zs \<longrightarrow> orules[preds := Ps] \<longrightarrow> P zs"}
 
-  If we assume @{text "pred zs"} and unfold its definition, then we have
+  If we assume @{text "pred zs"} and unfold its definition, then we have an
+  assumption
   
   @{text [display] "\<forall>preds. orules \<longrightarrow> pred zs"} 
 
-  and must prove
+  and must prove the goal
 
   @{text [display] "orules[preds := Ps] \<longrightarrow> P zs"}
 
@@ -119,23 +112,23 @@
   identity.
   
   Although the user declares introduction rules @{text rules}, they must 
-  be derived from the @{text defs}. These derivations are a bit involved. 
+  also be derived from the @{text defs}. These derivations are a bit involved. 
   Assuming we want to prove the introduction rule 
 
   @{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
 
-  then we can assume
+  then we can have assumptions of the form
 
   \begin{isabelle}
   (i)~~@{text "As"}\\
   (ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"}
   \end{isabelle}
 
-  and must show
+  and must show the goal
 
   @{text [display] "pred ts"}
   
-  If we now unfold the definitions for the @{text preds}, we have
+  If we now unfold the definitions for the @{text preds}, we have assumptions
 
   \begin{isabelle}
   (i)~~~@{text "As"}\\
@@ -155,13 +148,14 @@
   @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
 
   When we apply this rule we end up in the goal state where we have to prove
+  goals of the form
 
   \begin{isabelle}
   (a)~@{text "As"}\\
   (b)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"}
   \end{isabelle}
 
-  We can immediately discharge the goals @{text "As"} using the assumption in 
+  We can immediately discharge the goals @{text "As"} using the assumptions in 
   @{text "(i)"}. The goals in @{text "(b)"} can be discharged as follows: we 
   assume the @{text "Bs"} and prove @{text "pred ss"}. For this we resolve the 
   @{text "Bs"}  with the assumptions in @{text "(ii)"}. This gives us the 
@@ -173,8 +167,8 @@
   in @{text "(iii)"} gives us @{text "pred ss"}, which is the goal we are after.
   This completes the proof for introduction rules.
 
-  What remains is to implement the reasoning outlined above. We do this in
-  the next section. For building testcases, we use the shorthands for 
+  What remains is to implement the reasoning outlined in this section. We do this  
+  next. For building testcases, we use the shorthands for 
   @{text "even/odd"}, @{term "fresh"} and @{term "accpart"}
   given in Figure~\ref{fig:shorthands}.
 *}

--- a/ProgTutorial/Package/Ind_Interface.thy	Fri Mar 27 12:49:28 2009 +0000
+++ b/ProgTutorial/Package/Ind_Interface.thy	Fri Mar 27 18:19:42 2009 +0000
@@ -442,10 +442,12 @@
 *}
 
 text {*
-  From a high-level perspective the package consists of 6 subtasks:
+  (FIXME: perhaps move somewhere else)
 
-
-
+  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. For this 
+  it is instructive to look at the general construction principle 
+  of inductive definitions, which we shall do in the next section.
 *}
 
 

--- a/ProgTutorial/Package/Ind_Intro.thy	Fri Mar 27 12:49:28 2009 +0000
+++ b/ProgTutorial/Package/Ind_Intro.thy	Fri Mar 27 18:19:42 2009 +0000
@@ -33,12 +33,12 @@
   inductive predicates. To keep things really simple, we will not use the
   general Knaster-Tarski fixpoint theorem on complete lattices, which forms
   the basis of Isabelle's standard inductive definition package.  Instead, we
-  will use a simpler \emph{impredicative} (i.e.\ involving quantification on
+  will describe a simpler \emph{impredicative} (i.e.\ involving quantification on
   predicate variables) encoding of inductive predicates. Due to its
   simplicity, this package will necessarily have a reduced functionality. It
   does neither support introduction rules involving arbitrary monotone
-  operators, nor does it prove case analysis (or inversion) rules. Moreover,
-  it only proves a weaker form of the induction principle for inductive
+  operators, nor does it prove case analysis rules (also called inversion rules). 
+  Moreover, it only proves a weaker form of the induction principle for inductive
   predicates.
 *}
 

Binary file progtutorial.pdf has changed