I think I really like how drule and drule_all work, but is there something
that walks the middle road? I mean drule only discharges one condition; and
drule_all needs all conditions to be discharged. It would be nice to have a
drule that discharges as many as possible and leave the rest as implicants.

Also it appears that drule_all does not check if the theorem is proved and
leaves ``P ==> P`` as a goal.

hol-info mailing list

Reply via email to