src/HOL/Tools/inductive_package.ML
changeset 10910 058775a575db
parent 10804 306aee77eadd
child 10988 e0016a009c17
equal deleted inserted replaced
10909:2bbb1797bbe2 10910:058775a575db
    38      intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
    38      intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
    39   val print_inductives: theory -> unit
    39   val print_inductives: theory -> unit
    40   val mono_add_global: theory attribute
    40   val mono_add_global: theory attribute
    41   val mono_del_global: theory attribute
    41   val mono_del_global: theory attribute
    42   val get_monos: theory -> thm list
    42   val get_monos: theory -> thm list
       
    43   val inductive_forall_name: string
       
    44   val inductive_forall_def: thm
       
    45   val rulify: thm -> thm
    43   val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text
    46   val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text
    44     -> theory -> theory
    47     -> theory -> theory
    45   val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
    48   val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
    46     -> theory -> theory
    49     -> theory -> theory
    47   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    50   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    67 val gfp_name = "Gfp.gfp";
    70 val gfp_name = "Gfp.gfp";
    68 val lfp_name = "Lfp.lfp";
    71 val lfp_name = "Lfp.lfp";
    69 val vimage_name = "Inverse_Image.vimage";
    72 val vimage_name = "Inverse_Image.vimage";
    70 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
    73 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
    71 
    74 
       
    75 val inductive_forall_name = "Inductive.forall";
       
    76 val inductive_forall_def = thm "forall_def";
    72 val inductive_conj_name = "Inductive.conj";
    77 val inductive_conj_name = "Inductive.conj";
    73 val inductive_conj_def = thm "conj_def";
    78 val inductive_conj_def = thm "conj_def";
    74 val inductive_conj = thms "inductive_conj";
    79 val inductive_conj = thms "inductive_conj";
    75 val inductive_atomize = thms "inductive_atomize";
    80 val inductive_atomize = thms "inductive_atomize";
    76 val inductive_rulify1 = thms "inductive_rulify1";
    81 val inductive_rulify1 = thms "inductive_rulify1";