src/HOL/Finite.thy

Now Datatype.occs_in_prems prints the necessary warning ITSELF.

It is also easier to invoke and even works if the induction variable
is a parameter (rather than a free variable).

(*  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