# HG changeset patch
# User wenzelm
# Date 951252320 -3600
# Node ID 493707fcd8a6859fff7f2be9b2b7fb3de7fbe17e
# Parent  2647b7fa65088c37c0a2dbe15ed2496da8cbd4c8
added cases_of, cases;

diff -r 2647b7fa6508 -r 493707fcd8a6 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Tue Feb 22 21:39:38 2000 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Tue Feb 22 21:45:20 2000 +0100
@@ -36,6 +36,8 @@
     {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
@@ -102,12 +104,30 @@
       handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
   in InductiveData.put tab_monos thy end;
 
-val get_monos = snd o InductiveData.get;
+
+(* cases rules *)
 
-fun put_monos thms thy = InductiveData.put (fst (InductiveData.get thy), thms) thy;
+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;
+
 fun mk_mono thm =
   let
     fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @