| changeset 50705 | 0e943b33d907 |
| parent 50020 | 6b9611abcd4c |
| child 51130 | 76d68444cd59 |
--- a/src/HOL/Metis_Examples/Sets.thy Thu Jan 03 17:10:12 2013 +0100 +++ b/src/HOL/Metis_Examples/Sets.thy Thu Jan 03 17:28:55 2013 +0100 @@ -11,7 +11,7 @@ imports Main begin -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] 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)) &