diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean
index c81e7a7eb..d3db0965b 100644
--- a/Manual/Elaboration.lean
+++ b/Manual/Elaboration.lean
@@ -99,7 +99,8 @@ Roughly speaking, Lean's processing of a source file can be divided into the fol
 
 : Kernel Checking
 
-  Lean's trusted kernel checks the output of the elaborator to ensure that it follows the rules of the type theory.
+  Lean's trusted kernel{margin}[To avoid trusting the elaborator when verifying a statement, one has to {keywordOf Lean.Parser.Command.print}`#print` the statement to get the elaborated type and manually verify that it expresses the desired statement.
+  This brings {keywordOf Lean.Parser.Command.print}`#print` into the trusted base.] checks the output of the elaborator to ensure that it follows the rules of the type theory.
 
 : Compilation