isabelle: src/ZF/Datatype.thy@6e074b41c735 (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	paulson
	Thu, 25 Sep 1997 13:23:41 +0200
changeset 3715	6e074b41c735
parent 2870	6d6fd10a9fdc
child 6053	8a1059aa01f0
permissions	-rw-r--r--