src/FOL/FOL.thy

--- a/src/FOL/FOL.thy	Thu Aug 29 16:15:11 2002 +0200
+++ b/src/FOL/FOL.thy	Fri Aug 30 16:42:45 2002 +0200
@@ -28,7 +28,14 @@
 
 use "blastdata.ML"
 setup Blast.setup
-use "FOL_lemmas2.ML"
+
+
+lemma ex1_functional: "[| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
+by blast
+
+ML {*
+val ex1_functional = thm "ex1_functional";
+*}
 
 use "simpdata.ML"
 setup simpsetup