src/Doc/Isar_Ref/Proof.thy

   \chref{ch:gen-tools} and \partref{part:hol}).
 
   \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 "goal_cases"} & : & @{text method} \\
     @{method_def "fact"} & : & @{text method} \\
     @{method_def "assumption"} & : & @{text method} \\
     @{method_def "this"} & : & @{text method} \\
     @{method_def (Pure) "rule"} & : & @{text method} \\
     @{attribute_def (Pure) "intro"} & : & @{text attribute} \\

     @{attribute_def "of"} & : & @{text attribute} \\
     @{attribute_def "where"} & : & @{text attribute} \\
   \end{matharray}
 
   @{rail \<open>
-    @@{method goals} (@{syntax name}*)
+    @@{method goal_cases} (@{syntax name}*)
     ;
     @@{method fact} @{syntax thmrefs}?
     ;
     @@{method (Pure) rule} @{syntax thmrefs}?
     ;

   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"} turns the current subgoals
+  \item @{method "goal_cases"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} turns the current subgoals
   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}