changeset 42103 | 6066a35f6678 |
parent 41144 | 509e51b7509a |
--- a/src/HOL/Metis_Examples/set.thy Thu Mar 24 17:49:27 2011 +0100 +++ b/src/HOL/Metis_Examples/set.thy Thu Mar 24 17:49:27 2011 +0100 @@ -9,6 +9,8 @@ imports Main begin +declare [[metis_new_skolemizer]] + lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) & (S(x,y) | ~S(y,z) | Q(Z,Z)) & (Q(X,y) | ~Q(y,Z) | S(X,X))"