diff -r 4c9401fbbdf7 -r c708dafe2220 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Thu Jun 25 16:56:04 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Thu Jun 25 21:45:00 2015 +0200
@@ -818,6 +818,7 @@
   \begin{matharray}{rcl}
     @{command_def "print_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\[0.5ex]
     @{method_def "-"} & : & @{text method} \\
+    @{method_def "goals"} & : & @{text method} \\
     @{method_def "fact"} & : & @{text method} \\
     @{method_def "assumption"} & : & @{text method} \\
     @{method_def "this"} & : & @{text method} \\
@@ -832,6 +833,8 @@
   \end{matharray}
 
   @{rail \<open>
+    @@{method goals} (@{syntax name}*)
+    ;
     @@{method fact} @{syntax thmrefs}?
     ;
     @@{method (Pure) rule} @{syntax thmrefs}?
@@ -861,12 +864,23 @@
   rule declarations of the classical reasoner
   (\secref{sec:classical}).
 
-  \item ``@{method "-"}'' (minus) does nothing but insert the forward
-  chaining facts as premises into the goal.  Note that command
-  @{command_ref "proof"} without any method actually performs a single
-  reduction step using the @{method_ref (Pure) rule} method; thus a plain
-  \emph{do-nothing} proof step would be ``@{command "proof"}~@{text
-  "-"}'' rather than @{command "proof"} alone.
+  \item ``@{method "-"}'' (minus) inserts the forward chaining facts as
+  premises into the goal, and nothing else.
+
+  Note that command @{command_ref "proof"} without any method actually
+  performs a single reduction step using the @{method_ref (Pure) rule}
+  method; thus a plain \emph{do-nothing} proof step would be ``@{command
+  "proof"}~@{text "-"}'' rather than @{command "proof"} alone.
+
+  \item @{method "goals"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} is like ``@{method "-"}'', but
+  the current subgoals are turned into cases within the context (see also
+  \secref{sec:cases-induct}). The specified case names are used if present;
+  otherwise cases are numbered starting from 1.
+
+  Invoking cases in the subsequent proof body via the @{command_ref case}
+  command will @{command fix} goal parameters, @{command assume} goal
+  premises, and @{command let} variable @{variable_ref ?case} refer to the
+  conclusion.
 
   \item @{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} composes some fact from
   @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from the current proof context)