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