| changeset 50705 | 0e943b33d907 |
| parent 47040 | 78e88d26f19d |
| child 58889 | 5b7a9633cfa8 |
--- a/src/HOL/Metis_Examples/Tarski.thy Thu Jan 03 17:10:12 2013 +0100 +++ b/src/HOL/Metis_Examples/Tarski.thy Thu Jan 03 17:28:55 2013 +0100 @@ -11,7 +11,7 @@ imports Main "~~/src/HOL/Library/FuncSet" begin -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] (*Many of these higher-order problems appear to be impossible using the current linkup. They often seem to need either higher-order unification