isabelle: src/ZF/Induct/ROOT.ML@bdb890782d4a (annotated)

12201 7198f403a2f9 added Term and Tree_Forest (from converted ZF/ex); wenzelm parents: 12190 diff changeset	1	(* Title: ZF/Induct/ROOT.ML
12089 34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF. paulson parents: diff changeset	2	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF. paulson parents: diff changeset	3	Copyright 2001 University of Cambridge
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF. paulson parents: diff changeset	4
12201 7198f403a2f9 added Term and Tree_Forest (from converted ZF/ex); wenzelm parents: 12190 diff changeset	5	Inductive definitions.
12089 34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF. paulson parents: diff changeset	6	*)
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF. paulson parents: diff changeset	7
23912 039ae566a4a2 simultaneous use_thys; wenzelm parents: 12229 diff changeset	8	use_thys [
12229 bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct; wenzelm parents: 12205 diff changeset	9	( Datatypes )
23912 039ae566a4a2 simultaneous use_thys; wenzelm parents: 12229 diff changeset	10	"Datatypes", (sample datatypes)
039ae566a4a2 simultaneous use_thys; wenzelm parents: 12229 diff changeset	11	"Binary_Trees", (binary trees)
039ae566a4a2 simultaneous use_thys; wenzelm parents: 12229 diff changeset	12	"Term", (recursion over the list functor)
039ae566a4a2 simultaneous use_thys; wenzelm parents: 12229 diff changeset	13	"Ntree", (variable-branching trees; function demo)
039ae566a4a2 simultaneous use_thys; wenzelm parents: 12229 diff changeset	14	"Tree_Forest", (mutual recursion)
039ae566a4a2 simultaneous use_thys; wenzelm parents: 12229 diff changeset	15	"Brouwer", (Infinite-branching trees)
039ae566a4a2 simultaneous use_thys; wenzelm parents: 12229 diff changeset	16	"Mutil", (mutilated chess board)
12190 32a9c240f225 added Datatypes, Binary_Trees (from ZF/ex); wenzelm parents: 12089 diff changeset	17
12089 34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF. paulson parents: diff changeset	18	(*by Sidi Ehmety: Multisets. A parent is FoldSet, the "fold" function for
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF. paulson parents: diff changeset	19	finite sets*)
23912 039ae566a4a2 simultaneous use_thys; wenzelm parents: 12229 diff changeset	20	"Multiset",
039ae566a4a2 simultaneous use_thys; wenzelm parents: 12229 diff changeset	21	"Rmap", (mapping a relation over a list)
039ae566a4a2 simultaneous use_thys; wenzelm parents: 12229 diff changeset	22	"PropLog", (completeness of propositional logic)
12089 34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF. paulson parents: diff changeset	23
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF. paulson parents: diff changeset	24	(two Coq examples by Christine Paulin-Mohring)
23912 039ae566a4a2 simultaneous use_thys; wenzelm parents: 12229 diff changeset	25	"ListN",
039ae566a4a2 simultaneous use_thys; wenzelm parents: 12229 diff changeset	26	"Acc",
12089 34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF. paulson parents: diff changeset	27
23912 039ae566a4a2 simultaneous use_thys; wenzelm parents: 12229 diff changeset	28	"Comb", (Combinatory Logic example)
039ae566a4a2 simultaneous use_thys; wenzelm parents: 12229 diff changeset	29	"Primrec" (Primitive recursive functions)
039ae566a4a2 simultaneous use_thys; wenzelm parents: 12229 diff changeset	30	];

author	blanchet
	Fri, 22 Oct 2010 14:47:43 +0200
changeset 40070	bdb890782d4a
parent 35762	af3ff2ba4c54
permissions	-rw-r--r--