  We present PGT, a Proof Goal Transformer for Isabelle/HOL. Given a proof goal
and its background context, PGT attempts to generate conjectures from the
original goal by transforming the original proof goal. These conjectures should
be weak enough to be provable by automation but sufficiently strong to prove
the original goal. By incorporating PGT into the pre-existing PSL framework, we
exploit Isabelle's strong automation to identify and prove such conjectures.
