isabelle: src/HOL/Inductive.thy@fb604f0e5640 (annotated)

7700 38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	1	(* Title: HOL/Inductive.thy
38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	2	ID: $Id$
38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	3	*)
1187 bc94f00e47ba Includes Sum.thy as a parent for mutual recursion lcp parents: 923 diff changeset	4
8343 fb604f0e5640 require NatDef; wenzelm parents: 8303 diff changeset	5	theory Inductive = Gfp + Prod + Sum + NatDef
7700 38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	6	files
8303 5e7037409118 early setup of induct_method; wenzelm parents: 7710 diff changeset	7	"Tools/induct_method.ML"
7700 38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	8	"Tools/inductive_package.ML"
38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	9	"Tools/datatype_aux.ML"
38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	10	"Tools/datatype_prop.ML"
38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	11	"Tools/datatype_rep_proofs.ML"
38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	12	"Tools/datatype_abs_proofs.ML"
38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	13	"Tools/datatype_package.ML"
38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	14	"Tools/primrec_package.ML":
6437 9bdfe07ba8e9 'HOL/inductive' theory data; wenzelm parents: 5105 diff changeset	15
8303 5e7037409118 early setup of induct_method; wenzelm parents: 7710 diff changeset	16	setup InductMethod.setup
6437 9bdfe07ba8e9 'HOL/inductive' theory data; wenzelm parents: 5105 diff changeset	17	setup InductivePackage.setup
7700 38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	18	setup DatatypePackage.setup
38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	19
7710 bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via berghofe parents: 7700 diff changeset	20	theorems [mono] =
bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via berghofe parents: 7700 diff changeset	21	subset_refl imp_refl disj_mono conj_mono ex_mono all_mono
bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via berghofe parents: 7700 diff changeset	22	Collect_mono in_mono vimage_mono
bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via berghofe parents: 7700 diff changeset	23	imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via berghofe parents: 7700 diff changeset	24	not_all not_ex
bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via berghofe parents: 7700 diff changeset	25	Ball_def Bex_def
6437 9bdfe07ba8e9 'HOL/inductive' theory data; wenzelm parents: 5105 diff changeset	26
9bdfe07ba8e9 'HOL/inductive' theory data; wenzelm parents: 5105 diff changeset	27	end

author	wenzelm
	Sat, 04 Mar 2000 13:25:09 +0100
changeset 8343	fb604f0e5640
parent 8303	5e7037409118
child 8482	bbc805ebc904
permissions	-rw-r--r--