author | paulson |
Mon, 29 Sep 1997 11:46:33 +0200 | |
changeset 3729 | 6be7cf5086ab |
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