--- a/ex/set.ML Fri Nov 19 11:36:23 1993 +0100
+++ b/ex/set.ML Thu Nov 25 10:04:02 1993 +0100
@@ -9,6 +9,13 @@
writeln"File HOL/ex/set.";
+(*** A unique fixpoint theorem --- fast/best/meson all fail ***)
+
+val [prem] = goal HOL.thy "?!x.f(g(x))=x ==> ?!y.g(f(y))=y";
+by(EVERY1[rtac (prem RS ex1E), rtac ex1I, etac arg_cong,
+ rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]);
+result();
+
(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
goal Set.thy "~ (? f:: 'a=>'a set. ! S. ? x. f(x) = S)";