all_cases / all_inducts;
authorwenzelm
Thu Feb 24 16:00:09 2000 +0100 (2000-02-24)
changeset 82934a0e17cf8f70
parent 8292 93e125b21220
child 8294 c50607ff9704
all_cases / all_inducts;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Feb 24 15:59:44 2000 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Feb 24 16:00:09 2000 +0100
     1.3 @@ -37,7 +37,8 @@
     1.4        induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
     1.5    val print_inductives: theory -> unit
     1.6    val cases_of: Sign.sg -> string -> thm
     1.7 -  val cases: Sign.sg -> thm list
     1.8 +  val all_cases: Sign.sg -> thm list
     1.9 +  val all_inducts: Sign.sg -> thm list
    1.10    val mono_add_global: theory attribute
    1.11    val mono_del_global: theory attribute
    1.12    val get_monos: theory -> thm list
    1.13 @@ -105,7 +106,7 @@
    1.14    in InductiveData.put tab_monos thy end;
    1.15  
    1.16  
    1.17 -(* cases rules *)
    1.18 +(* cases and induct rules *)
    1.19  
    1.20  fun cases_of sg name =
    1.21    let
    1.22 @@ -119,7 +120,8 @@
    1.23      | Some thm => thm)
    1.24    end;
    1.25  
    1.26 -fun cases sg = flat (map (#elims o #2 o #2) (Symtab.dest (#1 (InductiveData.get_sg sg))));
    1.27 +fun all_cases sg = flat (map (#elims o #2 o #2) (Symtab.dest (#1 (InductiveData.get_sg sg))));
    1.28 +fun all_inducts sg = map (#induct o #2 o #2) (Symtab.dest (#1 (InductiveData.get_sg sg)));
    1.29        
    1.30  
    1.31