equal
deleted
inserted
replaced
13 inductive "Fin(A)" |
13 inductive "Fin(A)" |
14 intrs |
14 intrs |
15 emptyI "{} : Fin(A)" |
15 emptyI "{} : Fin(A)" |
16 insertI "[| a: A; b: Fin(A) |] ==> insert a b : Fin(A)" |
16 insertI "[| a: A; b: Fin(A) |] ==> insert a b : Fin(A)" |
17 |
17 |
18 consts finite :: 'a set => bool |
18 constdefs |
19 defs finite_def "finite A == A : Fin(UNIV)" |
|
20 |
19 |
21 consts card :: 'a set => nat |
20 finite :: 'a set => bool |
22 defs card_def "card A == LEAST n. ? f. A = {f i |i. i<n}" |
21 "finite A == A : Fin(UNIV)" |
|
22 |
|
23 card :: 'a set => nat |
|
24 "card A == LEAST n. ? f. A = {f i |i. i<n}" |
23 |
25 |
24 end |
26 end |