isabelle: src/FOL/FOL_lemmas2.ML@f88a91ff8ac6 (annotated)

7355 4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: diff changeset	1
9264 051592f4236a removal of batch style, and tidying paulson parents: 7355 diff changeset	2	Goal "[\| EX! z. P(a,z); P(a,b); P(a,c) \|] ==> b = c";
7355 4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: diff changeset	3	by (Blast_tac 1);
4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: diff changeset	4	qed "ex1_functional";