| changeset 128 | 89669c58e506 |
| 127:d9527f97246e | 128:89669c58e506 |
|---|---|
1 (* Title: HOL/Finite.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 Finite powerset operator |
|
7 *) |
|
8 |
|
9 Finite = Lfp + |
|
10 consts Fin :: "'a set => 'a set set" |
|
11 |
|
12 inductive "Fin(A)" |
|
13 intrs |
|
14 emptyI "{} : Fin(A)" |
|
15 insertI "[| a: A; b: Fin(A) |] ==> insert(a,b) : Fin(A)" |
|
16 |
|
17 end |