src/HOL/Datatype.thy
author berghofe
Fri Oct 23 22:34:18 1998 +0200 (1998-10-23)
changeset 5759 bf5d9e5b8cdf
parent 5714 b4f2e281a907
child 10212 33fe2d701ddd
permissions -rw-r--r--
unit and bool are now represented as datatypes.
     1 (*  Title:      HOL/Datatype.thy
     2     ID:         $Id$
     3     Author:     Stefan Berghofer
     4     Copyright   1998  TU Muenchen
     5 *)
     6 
     7 Datatype = Univ +
     8 
     9 rep_datatype bool
    10   distinct True_not_False, False_not_True
    11   induct   bool_induct
    12 
    13 rep_datatype sum
    14   distinct Inl_not_Inr, Inr_not_Inl
    15   inject   Inl_eq, Inr_eq
    16   induct   sum_induct
    17 
    18 rep_datatype prod
    19   inject   Pair_eq
    20   induct   prod_induct
    21 
    22 rep_datatype unit
    23   induct   unit_induct
    24 
    25 end