isabelle: src/ZF/Datatype.thy@b279a84ac11c (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
2870 6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it paulson parents: 809 diff changeset	11	Datatype = "constructor" + Inductive + Univ + QUniv +
6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it paulson parents: 809 diff changeset	12
6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it paulson parents: 809 diff changeset	13	end
6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it paulson parents: 809 diff changeset	14

author	wenzelm
	Mon, 16 Nov 1998 10:41:08 +0100
changeset 5869	b279a84ac11c
parent 2870	6d6fd10a9fdc
child 6053	8a1059aa01f0
permissions	-rw-r--r--