# HG changeset patch
# User paulson
# Date 905157945 -7200
# Node ID d50c2783f941c2bf5db4bc05d0272bd2452487b9
# Parent  4a179dba527ae1f9d74409b4301ebea2ffb10202
new example

diff -r 4a179dba527a -r d50c2783f941 src/ZF/ex/misc.ML
--- a/src/ZF/ex/misc.ML	Mon Sep 07 10:43:31 1998 +0200
+++ b/src/ZF/ex/misc.ML	Mon Sep 07 10:45:45 1998 +0200
@@ -9,6 +9,11 @@
 
 writeln"ZF/ex/misc";
 
+(*trivial example of term synthesis: apparently hard for some provers!*)
+Goal "a ~= b ==> a:?X & b ~: ?X";
+by (Blast_tac 1);
+result();
+
 (*Nice Blast_tac benchmark.  Proved in 0.3s; old tactics can't manage it!*)
 Goal "ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
 by (Blast_tac 1);