| changeset 5181 | 4ba3787d9709 |
| child 5714 | b4f2e281a907 |
| 5180:d82a70766af0 | 5181:4ba3787d9709 |
|---|---|
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 sum |
|
10 distinct "[[Inl_not_Inr, Inr_not_Inl]]" |
|
11 inject "[[Inl_eq, Inr_eq]]" |
|
12 induct sum_induct |
|
13 |
|
14 rep_datatype prod |
|
15 distinct "[[]]" |
|
16 inject "[[Pair_eq]]" |
|
17 induct "allI RS (allI RS (split_paired_All RS iffD2)) RS spec" |
|
18 |
|
19 end |