--- a/src/Doc/IsarRef/Document_Preparation.thy Mon May 13 13:01:10 2013 +0200
+++ b/src/Doc/IsarRef/Document_Preparation.thy Mon May 13 13:23:13 2013 +0200
@@ -358,7 +358,7 @@
or indentation for pretty printing of display material.
\item @{antiquotation_option_def goals_limit}~@{text "= nat"}
- determines the maximum number of goals to be printed (for goal-based
+ determines the maximum number of subgoals to be printed (for goal-based
antiquotation).
\item @{antiquotation_option_def source}~@{text "= bool"} prints the