I have spent some time constructing "forward proofs" using the theorem library in HOL. I am now hoping to move to applying tactics to make "backward proofs".
I am wondering if there is a way to, after a tactic has been applied, to view the list of theorems that the tactic applied, i.e., to reconstruct the forward proof in detail. This is mostly to help me understand how tactices work.
For example:
> g `x = 5 ==> 2*x = 10`;
val it = ...
> e (rw[]);
OK...
.
.
.
|- x = 5 ==> 2 * x = 10: proof
>
>
> list_steps(); (* or something similar? *)
REWRITE_RULE [...] t1
REWRITE_RULE [MULT] t2
REWRITE_RULE [MULT_ZERO] t3...
etc.
Thank you!
