# HG changeset patch
# User wenzelm
# Date 1005845854 -3600
# Node ID f368821d9c682e743be87fa9a466072cd6cba36a
# Parent  264f17d14ad9c221052a6c7161f4d6bcbf37bcaf
depends on Epsilon!

diff -r 264f17d14ad9 -r f368821d9c68 src/ZF/Finite.thy
--- a/src/ZF/Finite.thy	Thu Nov 15 18:36:24 2001 +0100
+++ b/src/ZF/Finite.thy	Thu Nov 15 18:37:34 2001 +0100
@@ -6,7 +6,7 @@
 Finite powerset operator
 *)
 
-Finite = Inductive + Nat +
+Finite = Inductive + Epsilon + Nat +
 
 (*The natural numbers as a datatype*)
 rep_datatype