src/HOL/Tools/inductive_package.ML
changeset 10910 058775a575db
parent 10804 306aee77eadd
child 10988 e0016a009c17
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Jan 16 00:30:06 2001 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Jan 16 00:32:38 2001 +0100
     1.3 @@ -40,6 +40,9 @@
     1.4    val mono_add_global: theory attribute
     1.5    val mono_del_global: theory attribute
     1.6    val get_monos: theory -> thm list
     1.7 +  val inductive_forall_name: string
     1.8 +  val inductive_forall_def: thm
     1.9 +  val rulify: thm -> thm
    1.10    val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text
    1.11      -> theory -> theory
    1.12    val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
    1.13 @@ -69,6 +72,8 @@
    1.14  val vimage_name = "Inverse_Image.vimage";
    1.15  val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
    1.16  
    1.17 +val inductive_forall_name = "Inductive.forall";
    1.18 +val inductive_forall_def = thm "forall_def";
    1.19  val inductive_conj_name = "Inductive.conj";
    1.20  val inductive_conj_def = thm "conj_def";
    1.21  val inductive_conj = thms "inductive_conj";