diff -r 6079c5a92757 -r da15d528fb19 ex/set.ML
--- 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)";