author | clasohm |
Wed, 06 Mar 1996 14:12:24 +0100 | |
changeset 1556 | 2fd82cec17d4 |
parent 1531 | e5eb247ad13c |
child 3367 | 832c245d967c |
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 = Arith + consts Fin :: 'a set => 'a set set inductive "Fin(A)" intrs emptyI "{} : Fin(A)" insertI "[| a: A; b: Fin(A) |] ==> insert a b : Fin(A)" constdefs finite :: 'a set => bool "finite A == A : Fin(UNIV)" card :: 'a set => nat "card A == LEAST n. ? f. A = {f i |i. i<n}" end