Is it possible to see how
metis manages to finish a proof?
My current proof ends with:
apply (auto simp add: fun_eq_iff morph_comp_def split: if_splits) apply metis by metis
And I would like to drop the two
metis_verbose, but I don't know how to read the output,
using [[metis_trace]] by metis.
Robert Soeldner has marked this topic as resolved.
Last updated: Dec 07 2023 at 20:16 UTC