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

12175 5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 6070 diff changeset	1	(* Title: ZF/Datatype.thy
2870 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
12175 5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 6070 diff changeset	6	(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory.
2870 6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it paulson parents: 809 diff changeset	7	*)
516 1957113f0d7d installation of new inductive/datatype sections lcp parents: 124 diff changeset	8
12175 5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 6070 diff changeset	9	theory Datatype = Inductive + Univ + QUniv
12183 c10cea75dd56 adapted primrec/datatype to Isar; wenzelm parents: 12175 diff changeset	10	files
c10cea75dd56 adapted primrec/datatype to Isar; wenzelm parents: 12175 diff changeset	11	"Tools/datatype_package.ML"
c10cea75dd56 adapted primrec/datatype to Isar; wenzelm parents: 12175 diff changeset	12	"Tools/numeral_syntax.ML": (belongs to theory Bin)
12175 5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 6070 diff changeset	13
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 6070 diff changeset	14	end

author	wenzelm
	Wed, 14 Nov 2001 18:46:30 +0100
changeset 12183	c10cea75dd56
parent 12175	5cf58a1799a7
child 13328	703de709a64b
permissions	-rw-r--r--