ex/Finite.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/Finite.thy	Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,5 @@
+Finite = Lfp +
+consts Fin :: "'a set => 'a set set"
+rules
+ Fin_def "Fin(A) == lfp(%F. insert({}, UN x:A. insert(x)``F))"
+end