X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=8714eae88f924c42f7ba6560530d3094be741f07;hp=8fe37ad2be182d92c8cc1298794ced2cc6a99b9d;hb=3be23d511f494d473da5aabb67375e25073f7e2c;hpb=c3998b2b5a85bd4b5a47c1b2518739fe9948807f

diff --git a/week4.mdwn b/week4.mdwn
index 8fe37ad2..8714eae8 100644
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -217,7 +217,7 @@ and so on.
 
 #Typed lambda terms#
 
-Given a set of types `T`, we define the set of typed lambda terms <code>&Lamda;_T</code>,
+Given a set of types `T`, we define the set of typed lambda terms <code>&Lambda;_T</code>,
 which is the smallest set such that
 
 *    each type `t` has an infinite set of distinct variables, {x^t}_1,
@@ -227,12 +227,12 @@ which is the smallest set such that
      &sigma;, then the application `(M N)` has type &tau;.
 
 *    If a variable `a` has type &sigma;, and term `M` has type &tau;, 
-     then the abstract `&lambda; a M` has type `&sigma; --> &tau;`.
+     then the abstract <code>&lambda; a M</code> has type &sigma; --> &tau;.
 
 The definitions of types and of typed terms should be highly familiar
-to semanticists, except that instead of writing `&sigma; --> &tau;`,
-linguists (following Montague, who followed Church) write `<&sigma;,
-&tau;>`.  We will use the arrow notation, since it is more iconic.
+to semanticists, except that instead of writing &sigma; --> &tau;,
+linguists (following Montague, who followed Church) write <&sigma;,
+&tau;>.  We will use the arrow notation, since it is more iconic.
 
 Some examples (assume that `x` has type `o`):