# HG changeset patch
# User wenzelm
# Date 951404409 -3600
# Node ID 4a0e17cf8f70e3385477419448171581f48180fc
# Parent  93e125b212206b7eab29ca0445c7e9fdbd6c0daf
all_cases / all_inducts;

diff -r 93e125b21220 -r 4a0e17cf8f70 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Feb 24 15:59:44 2000 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Thu Feb 24 16:00:09 2000 +0100
@@ -37,7 +37,8 @@
       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 all_cases: Sign.sg -> thm list
+  val all_inducts: Sign.sg -> thm list
   val mono_add_global: theory attribute
   val mono_del_global: theory attribute
   val get_monos: theory -> thm list
@@ -105,7 +106,7 @@
   in InductiveData.put tab_monos thy end;
 
 
-(* cases rules *)
+(* cases and induct rules *)
 
 fun cases_of sg name =
   let
@@ -119,7 +120,8 @@
     | Some thm => thm)
   end;
 
-fun cases sg = flat (map (#elims o #2 o #2) (Symtab.dest (#1 (InductiveData.get_sg sg))));
+fun all_cases sg = flat (map (#elims o #2 o #2) (Symtab.dest (#1 (InductiveData.get_sg sg))));
+fun all_inducts sg = map (#induct o #2 o #2) (Symtab.dest (#1 (InductiveData.get_sg sg)));