author | oheimb |
Fri, 20 Feb 1998 16:00:18 +0100 | |
changeset 4637 | bac998af6ea2 |
parent 3413 | c1f63cc3a768 |
child 5101 | 52e7c75acfe6 |
permissions | -rw-r--r-- |
(* Title: HOL/Finite.thy ID: $Id$ Author: Lawrence C Paulson & Tobias Nipkow Copyright 1995 University of Cambridge & TU Muenchen Finite sets and their cardinality *) Finite = Divides + Power + consts Finites :: 'a set set inductive "Finites" intrs emptyI "{} : Finites" insertI "A : Finites ==> insert a A : Finites" syntax finite :: 'a set => bool translations "finite A" == "A : Finites" constdefs card :: 'a set => nat "card A == LEAST n. ? f. A = {f i |i. i<n}" end