src/HOL/Datatype.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10212 33fe2d701ddd
child 11954 3d1780208bf3
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5181
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Datatype.thy
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
     2
    ID:         $Id$
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
     3
    Author:     Stefan Berghofer
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
     4
    Copyright   1998  TU Muenchen
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
     5
*)
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
     6
10212
33fe2d701ddd *** empty log message ***
nipkow
parents: 5759
diff changeset
     7
Datatype = Datatype_Universe +
5181
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
     8
5759
bf5d9e5b8cdf unit and bool are now represented as datatypes.
berghofe
parents: 5714
diff changeset
     9
rep_datatype bool
bf5d9e5b8cdf unit and bool are now represented as datatypes.
berghofe
parents: 5714
diff changeset
    10
  distinct True_not_False, False_not_True
bf5d9e5b8cdf unit and bool are now represented as datatypes.
berghofe
parents: 5714
diff changeset
    11
  induct   bool_induct
bf5d9e5b8cdf unit and bool are now represented as datatypes.
berghofe
parents: 5714
diff changeset
    12
5181
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
    13
rep_datatype sum
5714
b4f2e281a907 Changed syntax of rep_datatype.
berghofe
parents: 5181
diff changeset
    14
  distinct Inl_not_Inr, Inr_not_Inl
b4f2e281a907 Changed syntax of rep_datatype.
berghofe
parents: 5181
diff changeset
    15
  inject   Inl_eq, Inr_eq
5181
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
    16
  induct   sum_induct
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
    17
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
    18
rep_datatype prod
5714
b4f2e281a907 Changed syntax of rep_datatype.
berghofe
parents: 5181
diff changeset
    19
  inject   Pair_eq
b4f2e281a907 Changed syntax of rep_datatype.
berghofe
parents: 5181
diff changeset
    20
  induct   prod_induct
5181
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
    21
5759
bf5d9e5b8cdf unit and bool are now represented as datatypes.
berghofe
parents: 5714
diff changeset
    22
rep_datatype unit
bf5d9e5b8cdf unit and bool are now represented as datatypes.
berghofe
parents: 5714
diff changeset
    23
  induct   unit_induct
bf5d9e5b8cdf unit and bool are now represented as datatypes.
berghofe
parents: 5714
diff changeset
    24
5181
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
    25
end