avoid relying on "Thm.definitionK" to pick up definitions -- this was an old hack related to locales (to avoid expanding locale constants to their low-level definition) that is no longer necessary
no_document use_thys ["~~/src/HOL/Library/While_Combinator"];
use_thys ["MicroJava"];