src/HOL/Datatype.thy
author berghofe
Fri Jul 24 13:00:36 1998 +0200 (1998-07-24)
changeset 5181 4ba3787d9709
child 5714 b4f2e281a907
permissions -rw-r--r--
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe@5181
     1
(*  Title:      HOL/Datatype.thy
berghofe@5181
     2
    ID:         $Id$
berghofe@5181
     3
    Author:     Stefan Berghofer
berghofe@5181
     4
    Copyright   1998  TU Muenchen
berghofe@5181
     5
*)
berghofe@5181
     6
berghofe@5181
     7
Datatype = Univ +
berghofe@5181
     8
berghofe@5181
     9
rep_datatype sum
berghofe@5181
    10
  distinct "[[Inl_not_Inr, Inr_not_Inl]]"
berghofe@5181
    11
  inject   "[[Inl_eq, Inr_eq]]"
berghofe@5181
    12
  induct   sum_induct
berghofe@5181
    13
berghofe@5181
    14
rep_datatype prod
berghofe@5181
    15
  distinct "[[]]"
berghofe@5181
    16
  inject   "[[Pair_eq]]"
berghofe@5181
    17
  induct   "allI RS (allI RS (split_paired_All RS iffD2)) RS spec"
berghofe@5181
    18
berghofe@5181
    19
end