doc-src/IsarRef/Thy/Proof.thy

   initially (via @{command_ref "then"}), and whether the final result
   is meant to solve some pending goal.
 
   Goals may consist of multiple statements, resulting in a list of
   facts eventually.  A pending multi-goal is internally represented as
-  a meta-level conjunction (printed as @{text "&&"}), which is usually
+  a meta-level conjunction (@{text "&&&"}), which is usually
   split into the corresponding number of sub-goals prior to an initial
   method application, via @{command_ref "proof"}
   (\secref{sec:proof-steps}) or @{command_ref "apply"}
   (\secref{sec:tactic-commands}).  The @{method_ref induct} method
   covered in \secref{sec:cases-induct} acts on multiple claims