diff --git a/src/Ledger/Address.lagda b/src/Ledger/Address.lagda
index f5c46c8b9..82251a7ca 100644
--- a/src/Ledger/Address.lagda
+++ b/src/Ledger/Address.lagda
@@ -15,9 +15,9 @@ credential contains a hash, either of a verifying (public) key
 (\isVKey) or of a (\isScript).
 
 N.B.~in the Shelley era the type of the \stake field of the
-\BaseAddr record was \CredentialType; to specify an address with
-no stake, we would use an ``enterprise'' address. In contrast,
-the type of \stake in the Conway era is \Maybe~\CredentialType,
+\BaseAddr record was \CredentialType (see~\cite[Sec.~4]{cardano_shelley_spec});
+to specify an address with no stake, we would use an ``enterprise'' address.
+In contrast, the type of \stake in the Conway era is \Maybe~\CredentialType,
 so we can now use \BaseAddr to specify an address with no stake
 by setting \stake to \nothing.
 
diff --git a/src/Ledger/Certs.lagda b/src/Ledger/Certs.lagda
index 352b9dd45..4711097f8 100644
--- a/src/Ledger/Certs.lagda
+++ b/src/Ledger/Certs.lagda
@@ -217,7 +217,8 @@ private variable
 In the Conway era, support for pointer addresses, genesis delegations
 and MIR certificates is removed. In \DState, this means that the four
 fields relating to those features are no longer present, and \DelegEnv
-contains none of the fields it used to in the Shelley era.
+contains none of the fields it used to in the Shelley
+era~(\cite[Sec.~9.2]{cardano_shelley_spec}).
 
 Note that pointer addresses are still usable, only their staking
 functionality has been retired. So all funds locked behind pointer