author | wenzelm |
Thu, 16 Oct 1997 15:33:06 +0200 | |
changeset 3906 | 5ae0e1324c56 |
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