src/HOL/Datatype.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10212 33fe2d701ddd
child 11954 3d1780208bf3
permissions -rw-r--r--
improved theory reference in comment
     1 (*  Title:      HOL/Datatype.thy
     2     ID:         $Id$
     3     Author:     Stefan Berghofer
     4     Copyright   1998  TU Muenchen
     5 *)
     6 
     7 Datatype = Datatype_Universe +
     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