src/FOL/FOL_lemmas2.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/FOL_lemmas2.ML	Wed Aug 25 20:45:19 1999 +0200
@@ -0,0 +1,4 @@
+
+Goal "!!a b c. [| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c";
+  by (Blast_tac 1);
+qed "ex1_functional";