New theory Datatype. Needed as an ancestor when defining datatypes.
authorberghofe
Fri Jul 24 13:00:36 1998 +0200 (1998-07-24)
changeset 51814ba3787d9709
parent 5180 d82a70766af0
child 5182 69917bbbce45
New theory Datatype. Needed as an ancestor when defining datatypes.
src/HOL/Datatype.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Datatype.thy	Fri Jul 24 13:00:36 1998 +0200
     1.3 @@ -0,0 +1,19 @@
     1.4 +(*  Title:      HOL/Datatype.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Stefan Berghofer
     1.7 +    Copyright   1998  TU Muenchen
     1.8 +*)
     1.9 +
    1.10 +Datatype = Univ +
    1.11 +
    1.12 +rep_datatype sum
    1.13 +  distinct "[[Inl_not_Inr, Inr_not_Inl]]"
    1.14 +  inject   "[[Inl_eq, Inr_eq]]"
    1.15 +  induct   sum_induct
    1.16 +
    1.17 +rep_datatype prod
    1.18 +  distinct "[[]]"
    1.19 +  inject   "[[Pair_eq]]"
    1.20 +  induct   "allI RS (allI RS (split_paired_All RS iffD2)) RS spec"
    1.21 +
    1.22 +end