src/ZF/Finite.thy
changeset 12214 f368821d9c68
parent 12175 5cf58a1799a7
child 13194 812b00ed1c03
     1.1 --- a/src/ZF/Finite.thy	Thu Nov 15 18:36:24 2001 +0100
     1.2 +++ b/src/ZF/Finite.thy	Thu Nov 15 18:37:34 2001 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  Finite powerset operator
     1.5  *)
     1.6  
     1.7 -Finite = Inductive + Nat +
     1.8 +Finite = Inductive + Epsilon + Nat +
     1.9  
    1.10  (*The natural numbers as a datatype*)
    1.11  rep_datatype