isabelle: src/HOL/Inductive.thy@546686f0a6fb (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
8482 bbc805ebc904 Added setup for primrec theory data. berghofe parents: 8343 diff changeset	19	setup PrimrecPackage.setup
7700 38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	20
7710 bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via berghofe parents: 7700 diff changeset	21	theorems [mono] =
bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via berghofe parents: 7700 diff changeset	22	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	23	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	24	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	25	not_all not_ex
bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via berghofe parents: 7700 diff changeset	26	Ball_def Bex_def
6437 9bdfe07ba8e9 'HOL/inductive' theory data; wenzelm parents: 5105 diff changeset	27
9bdfe07ba8e9 'HOL/inductive' theory data; wenzelm parents: 5105 diff changeset	28	end

author	wenzelm
	Tue, 03 Oct 2000 01:14:52 +0200
changeset 10131	546686f0a6fb
parent 8482	bbc805ebc904
child 10212	33fe2d701ddd
permissions	-rw-r--r--