isabelle: src/ZF/Datatype.thy@17ae63f82ad8 (annotated)

2870 6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it paulson parents: 809 diff changeset	1	(* Title: ZF/Datatype
6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it paulson parents: 809 diff changeset	2	ID: $Id$
6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it paulson parents: 809 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it paulson parents: 809 diff changeset	4	Copyright 1997 University of Cambridge
6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it paulson parents: 809 diff changeset	5
6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it paulson parents: 809 diff changeset	6	Dummy theory: brings in all ancestors needed for (Co)Datatype Declarations
124 858ab9a9b047 made pseudo theories for all ML files; clasohm parents: diff changeset	7
2870 6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it paulson parents: 809 diff changeset	8	"Datatype" must be capital to avoid conflicts with ML's "datatype"
6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it paulson parents: 809 diff changeset	9	*)
516 1957113f0d7d installation of new inductive/datatype sections lcp parents: 124 diff changeset	10
6070 032babd0120b ZF: the natural numbers as a datatype paulson parents: 6053 diff changeset	11	Datatype = Inductive + Univ + QUniv