theory Scratch
  imports Main
begin

lemma f: False
  by auto (* Fails *)

thm_oracles f (* Marked red in IDE, but no explanation *)

end