src/ZF/Finite.thy
changeset 9491 1a36151ee2fc
parent 6053 8a1059aa01f0
child 12175 5cf58a1799a7
     1.1 --- a/src/ZF/Finite.thy	Tue Aug 01 13:43:22 2000 +0200
     1.2 +++ b/src/ZF/Finite.thy	Tue Aug 01 15:28:21 2000 +0200
     1.3 @@ -6,7 +6,18 @@
     1.4  Finite powerset operator
     1.5  *)
     1.6  
     1.7 -Finite = Arith + Inductive +
     1.8 +Finite = Inductive + Nat +
     1.9 +
    1.10 +setup setup_datatypes
    1.11 +
    1.12 +(*The natural numbers as a datatype*)
    1.13 +rep_datatype 
    1.14 +  elim		natE
    1.15 +  induct	nat_induct
    1.16 +  case_eqns	nat_case_0, nat_case_succ
    1.17 +  recursor_eqns recursor_0, recursor_succ
    1.18 +
    1.19 +
    1.20  consts
    1.21    Fin       :: i=>i
    1.22    FiniteFun :: [i,i]=>i         ("(_ -||>/ _)" [61, 60] 60)