../../../Core_DOM/common/tests/Document_getElementById.thy