changeset 13550 | 5a176b8dda84 |
parent 12367 | 1cee8a0db392 |
child 14085 | 8dc3e532959a |
--- 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