--- a/doc-src/IsarRef/Thy/Proof.thy Wed Nov 19 18:15:31 2008 +0100
+++ b/doc-src/IsarRef/Thy/Proof.thy Thu Nov 20 00:03:47 2008 +0100
@@ -381,7 +381,7 @@
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"}