src/ZF/Datatype.thy
author nipkow
Sun, 05 Jan 2003 21:03:14 +0100
changeset 13771 6cd59cc885a1
parent 13328 703de709a64b
child 16417 9bc16273c2d4
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it
paulson
parents: 809
diff changeset
     6
*)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 124
diff changeset
     7
13328
703de709a64b better document preparation
paulson
parents: 12183
diff changeset
     8
header{*Datatype and CoDatatype Definitions*}
703de709a64b better document preparation
paulson
parents: 12183
diff changeset
     9
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 6070
diff changeset
    10
theory Datatype = Inductive + Univ + QUniv
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12175
diff changeset
    11
  files
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12175
diff changeset
    12
    "Tools/datatype_package.ML"
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12175
diff changeset
    13
    "Tools/numeral_syntax.ML":  (*belongs to theory Bin*)
12175
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 6070
diff changeset
    14
5cf58a1799a7 rearranged inductive package for Isar;
wenzelm
parents: 6070
diff changeset
    15
end