Email Gateway (Aug 22 2022 at 13:10): Email Gateway (Aug 22 2022 at 13:10):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I'm frequently using 'apply fact' in exploratory proofs, often mid-way
when refactoring apply scripts into proper Isar. Later, I'd like to
clean up even more and replace the "implicit" fact references with named
facts. It would be very useful if 'apply fact' printed something in the
output panel/tooltip/somewhere else with a link to the fact it used.
For example:
have "P x" ...
...
show "Q x" by (intro p_q) fact
(* clickable markup: "See ‹P x›")
Is there anyone else who would find that valuable?
Cheers
Lars
Last updated: Nov 21 2024 at 12:39 UTC