isabelle: src/HOL/Inductive.thy@38b6d2643630 (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
6437 9bdfe07ba8e9 'HOL/inductive' theory data; wenzelm parents: 5105 diff changeset	18
9bdfe07ba8e9 'HOL/inductive' theory data; wenzelm parents: 5105 diff changeset	19	end

author	wenzelm
	Mon, 04 Oct 1999 21:43:45 +0200
changeset 7700	38b6d2643630
parent 7357	d0e16da40ea2
child 7710	bf8cb3fc5d64
permissions	-rw-r--r--