diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean
index ba40baaa..4579a9bd 100644
--- a/Arm/Insts/Common.lean
+++ b/Arm/Insts/Common.lean
@@ -21,6 +21,10 @@ as source operands does not violate the Apple ABI.
 
 For details, see
 https://developer.apple.com/documentation/xcode/writing-arm64-code-for-apple-platforms#Respect-the-purpose-of-specific-CPU-registers
+
+Also see "Procedure Call Standard for the Arm 64-bit Architecture";
+the latest version is available at
+https://github.com/ARM-software/abi-aa/releases
 -/
 partial def GPRIndex.rand (lo := 0) (hi := 31) :
   IO (BitVec 5) := do
diff --git a/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean b/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean
index db4272d7..ff188462 100644
--- a/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean
+++ b/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean
@@ -105,11 +105,11 @@ partial def Conversion_between_FP_and_Int_cls.fmov_general.rand : IO (Option (Bi
         Rn := ← BitVec.rand 5,
         Rd := ← (if (lsb opcode 0) = 1#1 then
                 -- FPConvOp.FPConvOp_MOV_ItoF
-                -- GPR used as a source operand.
+                -- Destination operand is a SIMD&FP register.
                   BitVec.rand 5
                 else
                 -- FPConvOp.FPConvOp_MOV_FtoI
-                -- GPR used as a destination operand.
+                -- Destination operand is a GPR register.
                   GPRIndex.rand) }
     pure (inst.toBitVec32)