src/ZF/Finite.thy
changeset 6053 8a1059aa01f0
parent 1478 2b8c2a7547ab
child 9491 1a36151ee2fc
     1.1 --- a/src/ZF/Finite.thy	Mon Dec 28 16:58:11 1998 +0100
     1.2 +++ b/src/ZF/Finite.thy	Mon Dec 28 16:59:28 1998 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4    intrs
     1.5      emptyI  "0 : Fin(A)"
     1.6      consI   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"
     1.7 -  type_intrs "[empty_subsetI, cons_subsetI, PowI]"
     1.8 +  type_intrs empty_subsetI, cons_subsetI, PowI
     1.9    type_elims "[make_elim PowD]"
    1.10  
    1.11  inductive