diff --git a/doc/cprover-manual/memory-primitives.md b/doc/cprover-manual/memory-primitives.md
index 984ecd093ac..350c72471ff 100644
--- a/doc/cprover-manual/memory-primitives.md
+++ b/doc/cprover-manual/memory-primitives.md
@@ -16,7 +16,7 @@ pointers as having 64 bits. This can be changed by various options (see section
 
 Memory is represented in CBMC as a set of objects. Each object represents a
 contiguous sequence of bytes and is identified via a numeric object ID. For
-example, assuming integers of width 4 and chars of with 1, a global integer
+example, assuming integers of width 4 and chars of width 1, a global integer
 variable would correspond to an object of size 4, and memory allocated via
 `malloc(10)` would correspond to an object of size 10.
 
@@ -273,4 +273,3 @@ programs.
 
 <sup>1</sup> Pointers with negative offsets never point to memory objects.
 Negative values are used internally to detect pointer underflows.
-
diff --git a/src/goto-instrument/contracts/doc/user/contracts-quantifiers.md b/src/goto-instrument/contracts/doc/user/contracts-quantifiers.md
index a384423747c..5f92757123a 100644
--- a/src/goto-instrument/contracts/doc/user/contracts-quantifiers.md
+++ b/src/goto-instrument/contracts/doc/user/contracts-quantifiers.md
@@ -16,7 +16,7 @@ While quantified expressions with arbitrary Boolean expressions are supported wi
 Concretely, with the SAT backend, the following syntax must be used for quantifiers:
 
 ```
-__CPROVER_forall { *id* *type*; *range* => *boolean expression* }
+__CPROVER_forall { *id* *type*; *range* ==> *boolean expression* }
 __CPROVER_exists { *id* *type*; *range* && *boolean expression* }
 ```