changeset 41413 | 64cd30d6b0b8 |
parent 41144 | 509e51b7509a |
child 42103 | 6066a35f6678 |
--- a/src/HOL/Metis_Examples/Tarski.thy Wed Dec 29 13:51:17 2010 +0100 +++ b/src/HOL/Metis_Examples/Tarski.thy Wed Dec 29 17:34:41 2010 +0100 @@ -8,7 +8,7 @@ header {* The Full Theorem of Tarski *} theory Tarski -imports Main FuncSet +imports Main "~~/src/HOL/Library/FuncSet" begin (*Many of these higher-order problems appear to be impossible using the