diff --git a/docs/Syntax.md b/docs/Syntax.md
index f8f10d51..de1a771d 100644
--- a/docs/Syntax.md
+++ b/docs/Syntax.md
@@ -197,7 +197,7 @@ sign.  Examples:
     ()                // A tuple with no components
 
     { x = 1, y = 2 }  // A record with two fields, `x` and `y`
-    {}                // A record with no fileds
+    {}                // A record with no fields
 
 The components of tuples are identified by position, while the
 components of records are identified by their label, and so the
@@ -224,16 +224,16 @@ record.  For example:
 
     type T = { sign :: Bit, number :: [15] }
 
-    // Valid defintion:
+    // Valid definition:
     // the type of the record is known.
     isPositive : T -> Bit
     isPositive x = x.sign
 
-    // Invalid defintion:
+    // Invalid definition:
     // insufficient type information.
     badDef x = x.f
 
-The components of a tuple or a record may also be access by using
+The components of a tuple or a record may also be accessed using
 pattern matching.  Patterns for tuples and records mirror the syntax
 for constructing values: tuple patterns use parenthesis, while record
 patterns use braces.  Examples:
@@ -242,12 +242,13 @@ patterns use braces.  Examples:
 
     distance2 { x = xPos, y = yPos } = xPos ^^ 2 + yPos ^^ 2
 
-    f x = fst + snd where
+    f p = x + y where
+        (x, y) = p
 
 Sequences
 =========
 
-A sequence is a fixed-length collection of element of the same type.
+A sequence is a fixed-length collection of elements of the same type.
 The type of a finite sequence of length `n`, with elements of type `a`
 is `[n] a`.  Often, a finite sequence of bits, `[n] Bit`, is called a
 _word_.  We may abbreviate the type `[n] Bit` as `[n]`.  An infinite
@@ -306,8 +307,11 @@ Explicit Type Instantiation
 If `f` is a polymorphic value with type:
 
     f : { tyParam }
+    f = zero
 
-    f `{ tyParam = t }
+you can evaluate `f`, passing it a type parameter:
+
+    f `{ tyParam = 13 }
 
 
 Demoting Numeric Types to Values
@@ -319,7 +323,7 @@ following notation:
     `{t}
 
 Here `t` should be a type expression with numeric kind.  The resulting
-expression is a finite word, which is sufficiently large to accomodate
+expression is a finite word, which is sufficiently large to accommodate
 the value of the type:
 
     `{t} :: {w >= width t}. [w]
diff --git a/docs/Syntax.pdf b/docs/Syntax.pdf
index 09d8b343..6785f38e 100644
Binary files a/docs/Syntax.pdf and b/docs/Syntax.pdf differ
diff --git a/docs/Version2Changes.md b/docs/Version2Changes.md
index 79a21d72..037c638c 100644
--- a/docs/Version2Changes.md
+++ b/docs/Version2Changes.md
@@ -199,6 +199,23 @@ that can be compared to each other:
     Cryptol> :t (==)
     == : {a} (Cmp a) => a -> a -> Bit
 
+Tuple Projection Syntax
+-----------------------
+
+In Cryptol version 1, we used the `project` function to extract items out of a tuple.
+In Cryptol version 2, we use the same `.` notation as is used to extract items out
+of records. Further, the `project` function was 1-based (the first element is at index 1
+of the tuple), but the `.` version of project is now 0-based (so the first element is
+at index 0 of the tuple). So, in Cryptol version 1:
+
+    Cryptol> project(1,3,(1,2,3))
+    1
+
+in Cryptol version 2, becomes:
+
+    Cryptol> (1,2,3).0
+    1
+
 Properties (theorems in version 1)
 ----------------------------------
 
@@ -226,7 +243,7 @@ version 2, the `:modernize` command can help a lot. However it doesn't do the
 whole job for you. This section describes some limitations and suggests
 effective ways of translating your code.
 
-Syntatic limitations
+Syntactic limitations
 --------------------
 
 Currently, `:modernize`:
@@ -235,6 +252,7 @@ Currently, `:modernize`:
 * doesn't automatically translate `take(3,xs)` to ``take`{3}xs``,
 * doesn't translate `**` to `^^`,
 * doesn't turn `theorem` declarations into `property`'s.
+* doesn't convert tuple `project` to the new `.` syntax
 
 Feature requests have been filed for these limitations.
 
diff --git a/docs/Version2Changes.pdf b/docs/Version2Changes.pdf
index 1d824ba1..66d9d283 100644
Binary files a/docs/Version2Changes.pdf and b/docs/Version2Changes.pdf differ
diff --git a/docs/Version2Table.md b/docs/Version2Table.md
index 4957cf73..51e9284e 100644
--- a/docs/Version2Table.md
+++ b/docs/Version2Table.md
@@ -21,5 +21,6 @@ Summary of Changes
 `[0 ...]:[inf][8]`            |`[0 ..]:[inf][8]`                 | Both produce `[0 .. 255]`(repeated)
 `[9, 8 .. 0]`                 |`[9 -- 0]`                        | Step defines decreasing sequences
 `&&, ||, ^`                   |`&, |, ^`                         | Boolean operator syntax
+`(1,2,3).0 (== 1)`            |`project(1,3,(1,2,3)) (==1)`      | Tuple projection syntax (and 0-based)
 `property foo xs=...`         |`theorem foo: {xs}. xs==`...      | Properties replace theorems (see below)
 
diff --git a/docs/Version2Table.pdf b/docs/Version2Table.pdf
index 763f6315..fea8e56b 100644
Binary files a/docs/Version2Table.pdf and b/docs/Version2Table.pdf differ