Hi, I just started HOL and am really enjoying it quite a bit. One difficulty I find during interactive tactic proof sessions is to get hold of and manipulate assumptions. Right now I find myself using sg to write new subgoals and then metis_tac[] to prove the baby steps that could be easily proved with MP if I know how to select an assumption to apply to another. Is this difficulty by design? Should I be writing sml code instead of going with existing tactics?
Concrete example: if assumption #n1 says a -> b and assumption #n2 says a how can I add b to the assumptions? Of course it may be a little more complicated as #n1 may be !x. a -> c /\ d /\ b and I may only want b. Thanks, Haitao Zhang
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
