src/Doc/Isar_Ref/Proof.thy

   arguments passed to the @{method cases} method:
 
   \medskip
   \begin{tabular}{llll}
     facts           &                 & arguments   & rule \\\hline
+    @{text "\<turnstile> R"}   & @{method cases} &             & implicit rule @{text R} \\
                     & @{method cases} &             & classical case split \\
                     & @{method cases} & @{text t}   & datatype exhaustion (type of @{text t}) \\
     @{text "\<turnstile> A t"} & @{method cases} & @{text "\<dots>"} & inductive predicate/set elimination (of @{text A}) \\
     @{text "\<dots>"}     & @{method cases} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
   \end{tabular}