diff -r 18d758e38d85 -r 61ac1efe02c3 src/Doc/IsarRef/Inner_Syntax.thy
--- a/src/Doc/IsarRef/Inner_Syntax.thy	Mon May 13 13:01:10 2013 +0200
+++ b/src/Doc/IsarRef/Inner_Syntax.thy	Mon May 13 13:23:13 2013 +0200
@@ -213,7 +213,7 @@
   might look at terms more discretely.
 
   \item @{attribute goals_limit} controls the maximum number of
-  subgoals to be shown in goal output.
+  subgoals to be printed.
 
   \item @{attribute show_main_goal} controls whether the main result
   to be proven should be displayed.  This information might be