src/HOL/Tools/inductive_package.ML

   val unify_consts: Sign.sg -> term list -> term list -> term list * term list
   val get_inductive: theory -> string ->
     {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
       induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
   val print_inductives: theory -> unit
+  val cases_of: Sign.sg -> string -> thm
+  val cases: Sign.sg -> thm list
   val mono_add_global: theory attribute
   val mono_del_global: theory attribute
   val get_monos: theory -> thm list
   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
     theory attribute list -> ((bstring * term) * theory attribute list) list ->

     fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
     val tab_monos = foldl upd (InductiveData.get thy, names)
       handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
   in InductiveData.put tab_monos thy end;
 
+
+(* cases rules *)
+
+fun cases_of sg name =
+  let
+    fun find (None, (_, ({names, ...}, {elims, ...}): inductive_info)) =
+          assoc (names ~~ elims, name)
+      | find (some, _) = some;
+    val (tab, _) = InductiveData.get_sg sg;
+  in
+    (case Symtab.foldl find (None, tab) of
+      None => error ("Unknown (co)inductive set " ^ quote name)
+    | Some thm => thm)
+  end;
+
+fun cases sg = flat (map (#elims o #2 o #2) (Symtab.dest (#1 (InductiveData.get_sg sg))));
+      
+
+
+(** monotonicity rules **)
+
 val get_monos = snd o InductiveData.get;
-
 fun put_monos thms thy = InductiveData.put (fst (InductiveData.get thy), thms) thy;
-
-(** monotonicity rules **)
 
 fun mk_mono thm =
   let
     fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @
       (case concl_of thm of