[isabelle] Markup for 'fact'

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?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.