src/HOL/Finite.thy
changeset 923 ff1574a81019
child 1370 7361ac9b024d
equal deleted inserted replaced
922:196ca0973a6d 923:ff1574a81019
       
     1 (*  Title: 	HOL/Finite.thy
       
     2     ID:         $Id$
       
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
       
     4     Copyright   1994  University of Cambridge
       
     5 
       
     6 Finite powerset operator
       
     7 *)
       
     8 
       
     9 Finite = Lfp +
       
    10 consts Fin :: "'a set => 'a set set"
       
    11 
       
    12 inductive "Fin(A)"
       
    13   intrs
       
    14     emptyI  "{} : Fin(A)"
       
    15     insertI "[| a: A;  b: Fin(A) |] ==> insert a b : Fin(A)"
       
    16 
       
    17 end