X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week5_system_F.mdwn;h=86f1c75bb9eb48708797946ea766dd58fa96d6b5;hp=684f42be4087594c9c97768e7f7ef66bcca0bc5b;hb=d03fe382641cc8bc266184561d3c484deeb12ca1;hpb=e786697f406f29139f4116d13687b37e42594f81

diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
index 684f42be..86f1c75b 100644
--- a/topics/_week5_system_F.mdwn
+++ b/topics/_week5_system_F.mdwn
@@ -18,10 +18,10 @@ System F is due (independently) to Girard and Reynolds.
 It enhances the simply-typed lambda calculus with quantification over
 types.  In System F, you can say things like
 
-<code>&Gamma; &alpha; (\x.x):(&alpha; -> &alpha;)</code>
+<code>&Lambda; &alpha; (\x.x):(&alpha; -> &alpha;)</code>
 
 This says that the identity function maps arguments of type &alpha; to
-results of type &alpha;, for any choice of &alpha;.  So the &Gamma; is
+results of type &alpha;, for any choice of &alpha;.  So the &Lambda; is
 a universal quantifier over types.