src/Doc/IsarRef/HOL_Specific.thy

   \begin{matharray}{rcl}
     @{command_def (HOL) "primrec"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def (HOL) "fun"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def (HOL) "function"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
     @{command_def (HOL) "termination"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
+    @{command_def (HOL) "fun_cases"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   \end{matharray}
 
   @{rail "
     @@{command (HOL) primrec} @{syntax target}? @{syntax \"fixes\"} @'where' equations
     ;

     equations: (@{syntax thmdecl}? @{syntax prop} + '|')
     ;
     functionopts: '(' (('sequential' | 'domintros') + ',') ')'
     ;
     @@{command (HOL) termination} @{syntax term}?
+    ;
+    @@{command (HOL) fun_cases} (@{syntax thmdecl}? @{syntax prop} + @'and')
   "}
 
   \begin{description}
 
   \item @{command (HOL) "primrec"} defines primitive recursive

   termination proof for the previously defined function @{text f}.  If
   this is omitted, the command refers to the most recent function
   definition.  After the proof is closed, the recursive equations and
   the induction principle is established.
 
+  \item @{command (HOL) "fun_cases"} generates specialized elimination
+  rules for function equations. It expects one or more function equations
+  and produces rules that eliminate the given equalities, following the cases
+  given in the function definition.
   \end{description}
 
   Recursive definitions introduced by the @{command (HOL) "function"}
   command accommodate reasoning by induction (cf.\ @{method induct}):
   rule @{text "f.induct"} refers to a specific induction rule, with