author | lcp |
Fri, 12 Aug 1994 12:51:34 +0200 | |
changeset 516 | 1957113f0d7d |
child 534 | cd8bec47e175 |
permissions | -rw-r--r-- |
(* Title: ZF/Finite.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Finite powerset operator *) Finite = Arith + consts Fin :: "i=>i" inductive domains "Fin(A)" <= "Pow(A)" intrs emptyI "0 : Fin(A)" consI "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)" type_intrs "[empty_subsetI, cons_subsetI, PowI]" type_elims "[make_elim PowD]" end