src/HOL/Datatype.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 5759 bf5d9e5b8cdf
child 10212 33fe2d701ddd
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
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
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
     7
Datatype = Univ +
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