equal
deleted
inserted
replaced
15 emptyI "{} : Finites" |
15 emptyI "{} : Finites" |
16 insertI "A : Finites ==> insert a A : Finites" |
16 insertI "A : Finites ==> insert a A : Finites" |
17 |
17 |
18 syntax finite :: 'a set => bool |
18 syntax finite :: 'a set => bool |
19 translations "finite A" == "A : Finites" |
19 translations "finite A" == "A : Finites" |
|
20 |
|
21 axclass finite<term |
|
22 finite "finite UNIV" |
20 |
23 |
21 (* This definition, although traditional, is ugly to work with |
24 (* This definition, although traditional, is ugly to work with |
22 constdefs |
25 constdefs |
23 card :: 'a set => nat |
26 card :: 'a set => nat |
24 "card A == LEAST n. ? f. A = {f i |i. i<n}" |
27 "card A == LEAST n. ? f. A = {f i |i. i<n}" |