theory test2
  imports "test1"
begin

definition XX :: "int" where
"XX = 0"

locale test1
begin

definition HT :: "'a set" where
"HT \<equiv> {}"

lemma subset: "HT \<subseteq> {}" 
  by (simp add: HT_def) 
                 
end

locale test2 = test1
begin

lemma x: "HT = {}"
  using HT_def subset by blast

lemma y: "XX \<le> 0" 
  by (simp add: XX_def) 

end               
end