export inductive_forall_name, inductive_forall_def, rulify;
authorwenzelm
Tue Jan 16 00:32:38 2001 +0100 (2001-01-16 ago)
changeset 10910058775a575db
parent 10909 2bbb1797bbe2
child 10911 eb5721204b38
export inductive_forall_name, inductive_forall_def, rulify;
src/HOL/Tools/inductive_package.ML
     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";