| changeset 12214 | f368821d9c68 |
| parent 12175 | 5cf58a1799a7 |
| child 13194 | 812b00ed1c03 |
| 12213:264f17d14ad9 | 12214:f368821d9c68 |
|---|---|
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Finite powerset operator |
6 Finite powerset operator |
7 *) |
7 *) |
8 |
8 |
9 Finite = Inductive + Nat + |
9 Finite = Inductive + Epsilon + Nat + |
10 |
10 |
11 (*The natural numbers as a datatype*) |
11 (*The natural numbers as a datatype*) |
12 rep_datatype |
12 rep_datatype |
13 elim natE |
13 elim natE |
14 induct nat_induct |
14 induct nat_induct |