git is a pain

diff --combined topics/week7_eval_cl.mdwn
index 65b0200,8349a40..8349a40
--- 1/topics/week7_eval_cl.mdwn
--- 2/topics/_week7_eval_cl.mdwn
+++ b/topics/week7_eval_cl.mdwn
@@@ -15,22 -15,21 +15,21 @@@ recall tha
      ((\x.I)Ω) == ((\x.I)((\x.xx)(\x.xx)))
                     *      *
  
- There are two redexes in this term; we've marked the operative lambda
+ There are two redexes in this term; we've marked the operative lambdas
  with a star.  If we reduce the leftmost redex first, the term reduces
- to the normal form `I` in one step.  But if we reduce the left most
+ to the normal form `I` in one step.  But if we reduce the rightmost
  redex instead, the "reduced" form is `(\x.I)Ω` again, and we are in
  danger of entering an infinite loop.
  
- Thanks to the recent introduction of sum types (disjoint union), we
+ Thanks to the introduction of sum types (disjoint union) in the last lecture, we
  are now in a position to gain a deeper understanding of evaluation
- order by reasoning explicitly about evaluation by writing a program
- that evaluates terms.
+ order by writing a program that allows us to reasoning explicitly about evaluation.
  
  One thing we'll see is that it is all too easy for the evaluation
  order properties of an evaluator to depend on the evaluation order
  properties of the programming language in which the evaluator is
  written.  We would like to write an evaluator in which the order of
- evaluation is insensitive to the evaluator language.  The goal is to
+ evaluation is insensitive to the evaluator language.  That is, the goal is to
  find an order-insensitive way to reason about evaluation order.  We
  will not fully succeed in this first attempt, but we will make good
  progress.
@@@ -85,7 -84,7 +84,7 @@@ With sum types, we can define CL terms 
  This type definition says that a term in CL is either one of the three
  simple expressions (`I`, `K`, or `S`), or else a pair of CL
  expressions.  `App` stands for Functional Application.  With this type
- definition, we can encode skomega, as well as other terms whose
+ definition, we can encode Skomega, as well as other terms whose
  reduction behavior we want to try to control.
  
  Using pattern matching, it is easy to code the one-step reduction
@@@ -104,13 -103,13 +103,13 @@@ rules for CL
  
  The definition of `reduce_one_step` explicitly says that it expects
  its input argument `t` to have type `term`, and the second `:term`
- says that the type of the output it delivers as a result will be of
+ says that the type of the output the function delivers as a result will also be of
  type `term`.
  
  The type constructor `App` obscures things a bit, but it's still
  possible to see how the one-step reduction function is just the
- reduction rules for CL.  The OCaml interpreter shows us that the
- function faithfully recognizes that `KSI ~~> S`, and `skomega ~~>
+ reduction rules for CL.  The OCaml interpreter responses given above show us that the
+ function faithfully recognizes that `KSI ~~> S`, and that `Skomega ~~>
  I(SII)(I(SII))`.
  
  We can now say precisely what it means to be a redex in CL.
@@@ -144,7 -143,7 +143,7 @@@ that are not at the top level of the te
  Because we need to process subparts, and because the result after
  processing a subpart may require further processing, the recursive
  structure of our evaluation function has to be somewhat subtle.  To
- truly understand, you will need to do some sophisticated thinking
+ truly understand, we will need to do some sophisticated thinking
  about how recursion works.  
  
  We'll develop our full reduction function in two stages.  Once we have
@@@ -163,7 -162,7 +162,7 @@@ allowing the evaluator to recognize tha
      I (I K) ~~> I K ~~> K
  
  When trying to understand how recursive functions work, it can be
- extremely helpful to examining an execution trace of inputs and
+ extremely helpful to examine an execution trace of inputs and
  outputs.
  
      # #trace reduce_stage1;;
@@@ -197,8 -196,10 +196,10 @@@ But the reduction function as written a
      # reduce_stage1 (App (App (I, I), K));;
      - : term = App (App (I, I), K)
  
- Because the top-level term is not a redex to start with,
- `reduce_stage1` returns it without any evaluation.  What we want is to
+ The reason is that the top-level term is not a redex to start with,
+ so `reduce_stage1` returns it without any evaluation.  
+ 
+ What we want is to
  evaluate the subparts of a complex term.  We'll do this by evaluating
  the subparts of the top-level expression.
  
@@@ -215,7 -216,9 +216,9 @@@ Since we need access to the subterms, w
  input.  If the input is simple (the first three `match` cases), we
  return it without further processing.  But if the input is complex, we
  first process the subexpressions, and only then see if we have a redex
- at the top level.  To understand how this works, follow the trace
+ at the top level.  
+ 
+ To understand how this works, follow the trace
  carefully:
  
      # reduce (App(App(I,I),K));;
@@@ -263,7 -266,7 +266,7 @@@ reduction work to be done (there isn't)
  You can see in more detail what is going on by tracing both reduce
  and reduce_one_step, but that makes for some long traces.
  
- So we've solved our first problem: reduce recognizes that `IIK ~~>
+ So we've solved our first problem: `reduce` now recognizes that `IIK ~~>
  K`, as desired.
  
  Because the OCaml interpreter evaluates each subexpression in the
@@@ -278,7 -281,7 +281,7 @@@ the only way to get out is to kill the 
  
  Instead of performing the leftmost reduction first, and recognizing 
  that this term reduces to the normal form `I`, we get lost endlessly
- trying to reduce skomega.
+ trying to reduce Skomega.
  
  ## Laziness is hard to overcome