isabelle: src/HOL/Inductive.thy@5ef0b624aadb (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
7357 d0e16da40ea2 proper bootstrap of HOL theory and packages; wenzelm parents: 6437 diff changeset	5	theory Inductive = Gfp + Prod + Sum
7700 38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	6	files
38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	7	"Tools/inductive_package.ML"
38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	8	"Tools/datatype_aux.ML"
38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	9	"Tools/datatype_prop.ML"
38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	10	"Tools/datatype_rep_proofs.ML"
38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	11	"Tools/datatype_abs_proofs.ML"
38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	12	"Tools/datatype_package.ML"
38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	13	"Tools/primrec_package.ML":
6437 9bdfe07ba8e9 'HOL/inductive' theory data; wenzelm parents: 5105 diff changeset	14
9bdfe07ba8e9 'HOL/inductive' theory data; wenzelm parents: 5105 diff changeset	15	setup InductivePackage.setup
7700 38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	16	setup DatatypePackage.setup
38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	17
7710 bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via berghofe parents: 7700 diff changeset	18	theorems [mono] =
bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via berghofe parents: 7700 diff changeset	19	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	20	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	21	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	22	not_all not_ex
bf8cb3fc5d64 Monotonicity rules for inductive definitions can now be added to a theory via berghofe parents: 7700 diff changeset	23	Ball_def Bex_def
6437 9bdfe07ba8e9 'HOL/inductive' theory data; wenzelm parents: 5105 diff changeset	24
9bdfe07ba8e9 'HOL/inductive' theory data; wenzelm parents: 5105 diff changeset	25	end

author	oheimb
	Fri, 28 Jan 2000 11:22:02 +0100
changeset 8148	5ef0b624aadb
parent 7710	bf8cb3fc5d64
child 8303	5e7037409118
permissions	-rw-r--r--